![]() |
Metamath
Proof Explorer Theorem List (p. 289 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iswspthsnon 28801* | The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} | ||
Theorem | wwlknon 28802 | An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
⊢ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘𝑁) = 𝐵)) | ||
Theorem | wspthnon 28803* | An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 15-Mar-2022.) |
⊢ (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊)) | ||
Theorem | wspthnonp 28804* | Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊))) | ||
Theorem | wspthneq1eq2 28805 | Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.) |
⊢ ((𝑃 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ∧ 𝑃 ∈ (𝐶(𝑁 WSPathsNOn 𝐺)𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | wwlksn0s 28806* | The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (0 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1} | ||
Theorem | wwlkssswrd 28807 | Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (WWalks‘𝐺) ⊆ Word 𝑉 | ||
Theorem | wwlksn0 28808* | A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 21-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (0 WWalksN 𝐺) → ∃𝑣 ∈ 𝑉 𝑊 = 〈“𝑣”〉) | ||
Theorem | 0enwwlksnge1 28809 | In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ (((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) → (𝑁 WWalksN 𝐺) = ∅) | ||
Theorem | wwlkswwlksn 28810 | A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑊 ∈ (WWalks‘𝐺)) | ||
Theorem | wwlkssswwlksn 28811 | The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑁 WWalksN 𝐺) ⊆ (WWalks‘𝐺) | ||
Theorem | wlkiswwlks1 28812 | The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalks‘𝐺))) | ||
Theorem | wlklnwwlkln1 28813 | The sequence of vertices in a walk of length 𝑁 is a walk as word of length 𝑁 in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 𝑁) → 𝑃 ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wlkiswwlks2lem1 28814* | Lemma 1 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1)) | ||
Theorem | wlkiswwlks2lem2 28815* | Lemma 2 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ (((♯‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((♯‘𝑃) − 1))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) | ||
Theorem | wlkiswwlks2lem3 28816* | Lemma 3 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃:(0...(♯‘𝐹))⟶𝑉) | ||
Theorem | wlkiswwlks2lem4 28817* | Lemma 4 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | ||
Theorem | wlkiswwlks2lem5 28818* | Lemma 5 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) | ||
Theorem | wlkiswwlks2lem6 28819* | Lemma 6 for wlkiswwlks2 28820. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | ||
Theorem | wlkiswwlks2 28820* | A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) | ||
Theorem | wlkiswwlks 28821* | A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalks‘𝐺))) | ||
Theorem | wlkiswwlksupgr2 28822* | A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 28820 does not require 𝐺 to be a simple pseudograph, but it requires the Axiom of Choice (ac6 10416) for its proof. Notice that only the existence of a function 𝑓 can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 28820). (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) | ||
Theorem | wlkiswwlkupgr 28823* | A walk as word corresponds to a walk in a pseudograph. This variant of wlkiswwlks 28821 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (∃𝑓 𝑓(Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalks‘𝐺))) | ||
Theorem | wlkswwlksf1o 28824* | The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021.) |
⊢ 𝐹 = (𝑤 ∈ (Walks‘𝐺) ↦ (2nd ‘𝑤)) ⇒ ⊢ (𝐺 ∈ USPGraph → 𝐹:(Walks‘𝐺)–1-1-onto→(WWalks‘𝐺)) | ||
Theorem | wlkswwlksen 28825 | The set of walks as words and the set of (ordinary) walks are equinumerous in a simple pseudograph. (Contributed by AV, 6-May-2021.) (Revised by AV, 5-Aug-2022.) |
⊢ (𝐺 ∈ USPGraph → (Walks‘𝐺) ≈ (WWalks‘𝐺)) | ||
Theorem | wwlksm1edg 28826 | Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ 2 ≤ (♯‘𝑊)) → (𝑊 prefix ((♯‘𝑊) − 1)) ∈ (WWalks‘𝐺)) | ||
Theorem | wlklnwwlkln2lem 28827* | Lemma for wlklnwwlkln2 28828 and wlklnwwlklnupgr2 28830. Formerly part of proof for wlklnwwlkln2 28828. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝜑 → (𝑃 ∈ (WWalks‘𝐺) → ∃𝑓 𝑓(Walks‘𝐺)𝑃)) ⇒ ⊢ (𝜑 → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) | ||
Theorem | wlklnwwlkln2 28828* | A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) | ||
Theorem | wlklnwwlkn 28829* | A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wlklnwwlklnupgr2 28830* | A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a pseudograph. This variant of wlklnwwlkln2 28828 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁))) | ||
Theorem | wlklnwwlknupgr 28831* | A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a pseudograph. This variant of wlkiswwlks 28821 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑃 ∧ (♯‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wlknewwlksn 28832 | If a walk in a pseudograph has length 𝑁, then the sequence of the vertices of the walk is a word representing the walk as word of length 𝑁. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧ (♯‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalksN 𝐺)) | ||
Theorem | wlknwwlksnbij 28833* | The mapping (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.) |
⊢ 𝑇 = {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = (𝑁 WWalksN 𝐺) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊) | ||
Theorem | wlknwwlksnen 28834* | In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁} ≈ (𝑁 WWalksN 𝐺)) | ||
Theorem | wlknwwlksneqs 28835* | The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁}) = (♯‘(𝑁 WWalksN 𝐺))) | ||
Theorem | wwlkseq 28836* | Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ 𝑇 ∈ (WWalks‘𝐺)) → (𝑊 = 𝑇 ↔ ((♯‘𝑊) = (♯‘𝑇) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑇‘𝑖)))) | ||
Theorem | wwlksnred 28837 | Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wwlksnext 28838 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) | ||
Theorem | wwlksnextbi 28839 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Proof shortened by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ 〈“𝑆”〉) ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ 𝑇 ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wwlksnredwwlkn 28840* | For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸))) | ||
Theorem | wwlksnredwwlkn0 28841* | For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸))) | ||
Theorem | wwlksnextwrd 28842* | Lemma for wwlksnextbij 28847. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) | ||
Theorem | wwlksnextfun 28843* | Lemma for wwlksnextbij 28847. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷⟶𝑅) | ||
Theorem | wwlksnextinj 28844* | Lemma for wwlksnextbij 28847. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷–1-1→𝑅) | ||
Theorem | wwlksnextsurj 28845* | Lemma for wwlksnextbij 28847. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–onto→𝑅) | ||
Theorem | wwlksnextbij0 28846* | Lemma for wwlksnextbij 28847. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–1-1-onto→𝑅) | ||
Theorem | wwlksnextbij 28847* | There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}) | ||
Theorem | wwlksnexthasheq 28848* | The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) = (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸})) | ||
Theorem | disjxwwlksn 28849* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 prefix 𝑁) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} | ||
Theorem | wwlksnndef 28850 | Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) |
⊢ ((𝐺 ∉ V ∨ 𝑁 ∉ ℕ0) → (𝑁 WWalksN 𝐺) = ∅) | ||
Theorem | wwlksnfi 28851 | The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Proof shortened by JJ, 18-Nov-2022.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin) | ||
Theorem | wlksnfi 28852* | The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 20-Apr-2021.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (Walks‘𝐺) ∣ (♯‘(1st ‘𝑝)) = 𝑁} ∈ Fin) | ||
Theorem | wlksnwwlknvbij 28853* | There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 5-Aug-2022.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) | ||
Theorem | wwlksnextproplem1 28854 | Lemma 1 for wwlksnextprop 28857. (Contributed by Alexander van der Vekens, 31-Jul-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 prefix (𝑁 + 1))‘0) = (𝑊‘0)) | ||
Theorem | wwlksnextproplem2 28855 | Lemma 2 for wwlksnextprop 28857. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {(lastS‘(𝑊 prefix (𝑁 + 1))), (lastS‘𝑊)} ∈ 𝐸) | ||
Theorem | wwlksnextproplem3 28856* | Lemma 3 for wwlksnextprop 28857. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix (𝑁 + 1)) ∈ 𝑌) | ||
Theorem | wwlksnextprop 28857* | Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ (𝑁 ∈ ℕ0 → {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) | ||
Theorem | disjxwwlkn 28858* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} | ||
Theorem | hashwwlksnext 28859* | Number of walks (as words) extended by an edge as a sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) = Σ𝑦 ∈ 𝑌 (♯‘{𝑥 ∈ 𝑋 ∣ ((𝑥 prefix 𝑀) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)})) | ||
Theorem | wwlksnwwlksnon 28860* | A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 13-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) | ||
Theorem | wspthsnwspthsnon 28861* | A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-May-2021.) (Revised by AV, 13-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏)) | ||
Theorem | wspthsnonn0vne 28862 | If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝑋(𝑁 WSPathsNOn 𝐺)𝑌) ≠ ∅) → 𝑋 ≠ 𝑌) | ||
Theorem | wspthsswwlkn 28863 | The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length. (Contributed by AV, 18-May-2021.) |
⊢ (𝑁 WSPathsN 𝐺) ⊆ (𝑁 WWalksN 𝐺) | ||
Theorem | wspthnfi 28864 | In a finite graph, the set of simple paths of a fixed length is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 18-May-2021.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WSPathsN 𝐺) ∈ Fin) | ||
Theorem | wwlksnonfi 28865 | In a finite graph, the set of walks of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∈ Fin) | ||
Theorem | wspthsswwlknon 28866 | The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length between the two vertices. (Contributed by AV, 15-May-2021.) |
⊢ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ⊆ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) | ||
Theorem | wspthnonfi 28867 | In a finite graph, the set of simple paths of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ∈ Fin) | ||
Theorem | wspniunwspnon 28868* | The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐺 ∈ 𝑈) → (𝑁 WSPathsN 𝐺) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ (𝑉 ∖ {𝑥})(𝑥(𝑁 WSPathsNOn 𝐺)𝑦)) | ||
Theorem | wspn0 28869 | If there are no vertices, then there are no simple paths (of any length), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 13-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑉 = ∅ → (𝑁 WSPathsN 𝐺) = ∅) | ||
Theorem | 2wlkdlem1 28870 | Lemma 1 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1) | ||
Theorem | 2wlkdlem2 28871 | Lemma 2 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (0..^(♯‘𝐹)) = {0, 1} | ||
Theorem | 2wlkdlem3 28872 | Lemma 3 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵 ∧ (𝑃‘2) = 𝐶)) | ||
Theorem | 2wlkdlem4 28873* | Lemma 4 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) | ||
Theorem | 2wlkdlem5 28874* | Lemma 5 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 2pthdlem1 28875* | Lemma 1 for 2pthd 28885. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗))) | ||
Theorem | 2wlkdlem6 28876 | Lemma 6 for 2wlkd 28881. (Contributed by AV, 23-Jan-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾))) | ||
Theorem | 2wlkdlem7 28877 | Lemma 7 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V)) | ||
Theorem | 2wlkdlem8 28878 | Lemma 8 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾)) | ||
Theorem | 2wlkdlem9 28879 | Lemma 9 for 2wlkd 28881. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)))) | ||
Theorem | 2wlkdlem10 28880* | Lemma 10 for 3wlkd 29114. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 2wlkd 28881 | Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018.) (Revised by AV, 23-Jan-2021.) (Proof shortened by AV, 14-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | 2wlkond 28882 | A walk of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐶)𝑃) | ||
Theorem | 2trld 28883 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) ⇒ ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | 2trlond 28884 | A trail of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) ⇒ ⊢ (𝜑 → 𝐹(𝐴(TrailsOn‘𝐺)𝐶)𝑃) | ||
Theorem | 2pthd 28885 | A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | 2spthd 28886 | A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | 2pthond 28887 | A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Proof shortened by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐽 ≠ 𝐾) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐹(𝐴(SPathsOn‘𝐺)𝐶)𝑃) | ||
Theorem | 2pthon3v 28888* | For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(𝐴(SPathsOn‘𝐺)𝐶)𝑝 ∧ (♯‘𝑓) = 2)) | ||
Theorem | umgr2adedgwlklem 28889 | Lemma for umgr2adedgwlk 28890, umgr2adedgspth 28893, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | ||
Theorem | umgr2adedgwlk 28890 | In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) & ⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) & ⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → (𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 2 ∧ (𝐴 = (𝑃‘0) ∧ 𝐵 = (𝑃‘1) ∧ 𝐶 = (𝑃‘2)))) | ||
Theorem | umgr2adedgwlkon 28891 | In a multigraph, two adjacent edges form a walk between two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) & ⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) & ⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐶)𝑃) | ||
Theorem | umgr2adedgwlkonALT 28892 | Alternate proof for umgr2adedgwlkon 28891, using umgr2adedgwlk 28890, but with a much longer proof! In a multigraph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) & ⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) & ⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐶)𝑃) | ||
Theorem | umgr2adedgspth 28893 | In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸)) & ⊢ (𝜑 → (𝐼‘𝐽) = {𝐴, 𝐵}) & ⊢ (𝜑 → (𝐼‘𝐾) = {𝐵, 𝐶}) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | umgr2wlk 28894* | In a multigraph, there is a walk of length 2 for each pair of adjacent edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) | ||
Theorem | umgr2wlkon 28895* | For each pair of adjacent edges in a multigraph, there is a walk of length 2 between the not common vertices of the edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ∃𝑓∃𝑝 𝑓(𝐴(WalksOn‘𝐺)𝐶)𝑝) | ||
Theorem | elwwlks2s3 28896* | A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (2 WWalksN 𝐺) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) | ||
Theorem | midwwlks2s3 28897* | There is a vertex between the endpoints of a walk of length 2 between two vertices as length 3 string. (Contributed by AV, 10-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (2 WWalksN 𝐺) → ∃𝑏 ∈ 𝑉 (𝑊‘1) = 𝑏) | ||
Theorem | wwlks2onv 28898 | If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) (Proof shortened by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐵 ∈ 𝑈 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) | ||
Theorem | elwwlks2ons3im 28899 | A walk as word of length 2 between two vertices is a length 3 string and its second symbol is a vertex. (Contributed by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) → (𝑊 = 〈“𝐴(𝑊‘1)𝐶”〉 ∧ (𝑊‘1) ∈ 𝑉)) | ||
Theorem | elwwlks2ons3 28900* | For each walk of length 2 between two vertices, there is a third vertex in the middle of the walk. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |