Home | Metamath
Proof Explorer Theorem List (p. 277 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wwlksnredwwlkn 27601* | 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 27602* | 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 27603* | Lemma for wwlksnextbij 27608. (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 27604* | Lemma for wwlksnextbij 27608. (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 27605* | Lemma for wwlksnextbij 27608. (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 27606* | Lemma for wwlksnextbij 27608. (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 27607* | Lemma for wwlksnextbij 27608. (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 27608* | 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 27609* | 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 27610* | 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 27611 | 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 27612 | 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 | wwlksnfiOLD 27613 | Obsolete version of wwlksnfiOLD 27613 as of 4-May-2023. (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin) | ||
Theorem | wlksnfi 27614* | 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 27615* | 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 27616 | Lemma 1 for wwlksnextprop 27619. (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 27617 | Lemma 2 for wwlksnextprop 27619. (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 27618* | Lemma 3 for wwlksnextprop 27619. (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 27619* | 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 27620* | 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 27621* | 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 27622* | 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 27623* | 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 27624 | 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 27625 | 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 27626 | 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 27627 | 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 27628 | 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 27629 | 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 27630* | 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 27631 | 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 27632 | Lemma 1 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1) | ||
Theorem | 2wlkdlem2 27633 | Lemma 2 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (0..^(♯‘𝐹)) = {0, 1} | ||
Theorem | 2wlkdlem3 27634 | Lemma 3 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵 ∧ (𝑃‘2) = 𝐶)) | ||
Theorem | 2wlkdlem4 27635* | Lemma 4 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) | ||
Theorem | 2wlkdlem5 27636* | Lemma 5 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 2pthdlem1 27637* | Lemma 1 for 2pthd 27647. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗))) | ||
Theorem | 2wlkdlem6 27638 | Lemma 6 for 2wlkd 27643. (Contributed by AV, 23-Jan-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾))) | ||
Theorem | 2wlkdlem7 27639 | Lemma 7 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V)) | ||
Theorem | 2wlkdlem8 27640 | Lemma 8 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾)) | ||
Theorem | 2wlkdlem9 27641 | Lemma 9 for 2wlkd 27643. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)))) | ||
Theorem | 2wlkdlem10 27642* | Lemma 10 for 3wlkd 27877. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 2wlkd 27643 | 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 27644 | 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 27645 | 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 27646 | 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 27647 | 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 27648 | 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 27649 | 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 27650* | 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 27651 | Lemma for umgr2adedgwlk 27652, umgr2adedgspth 27655, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | ||
Theorem | umgr2adedgwlk 27652 | 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 27653 | 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 27654 | Alternate proof for umgr2adedgwlkon 27653, using umgr2adedgwlk 27652, 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 27655 | 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 27656* | 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 27657* | 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 27658* | A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (2 WWalksN 𝐺) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) | ||
Theorem | midwwlks2s3 27659* | 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 27660 | 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 27661 | 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 27662* | 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 𝐺)𝐶))) | ||
Theorem | s3wwlks2on 27663* | A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑓(𝑓(Walks‘𝐺)〈“𝐴𝐵𝐶”〉 ∧ (♯‘𝑓) = 2))) | ||
Theorem | umgrwwlks2on 27664 | A walk of length 2 between two vertices as word in a multigraph. This theorem would also hold for pseudographs, but to prove this the cases 𝐴 = 𝐵 and/or 𝐵 = 𝐶 must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) | ||
Theorem | wwlks2onsym 27665 | There is a walk of length 2 from one vertex to another vertex iff there is a walk of length 2 from the other vertex to the first vertex. (Contributed by AV, 7-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ 〈“𝐶𝐵𝐴”〉 ∈ (𝐶(2 WWalksNOn 𝐺)𝐴))) | ||
Theorem | elwwlks2on 27666* | A walk of length 2 between two vertices as length 3 string. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WWalksNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))) | ||
Theorem | elwspths2on 27667* | A simple path of length 2 between two vertices (in a graph) as length 3 string. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑊 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = 〈“𝐴𝑏𝐶”〉 ∧ 〈“𝐴𝑏𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶)))) | ||
Theorem | wpthswwlks2on 27668 | For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 13-May-2021.) (Revised by AV, 16-Mar-2022.) |
⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵) → (𝐴(2 WSPathsNOn 𝐺)𝐵) = (𝐴(2 WWalksNOn 𝐺)𝐵)) | ||
Theorem | 2wspdisj 27669* | All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 9-Jan-2022.) |
⊢ Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(2 WSPathsNOn 𝐺)𝑏) | ||
Theorem | 2wspiundisj 27670* | All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) (Revised by AV, 14-May-2021.) (Proof shortened by AV, 9-Jan-2022.) |
⊢ Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(2 WSPathsNOn 𝐺)𝑏) | ||
Theorem | usgr2wspthons3 27671 | A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈“𝐴𝐵𝐶”〉 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸))) | ||
Theorem | usgr2wspthon 27672* | A simple path of length 2 between two vertices corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(2 WSPathsNOn 𝐺)𝐶) ↔ ∃𝑏 ∈ 𝑉 ((𝑇 = 〈“𝐴𝑏𝐶”〉 ∧ 𝐴 ≠ 𝐶) ∧ ({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝐶} ∈ 𝐸)))) | ||
Theorem | elwwlks2 27673* | A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) | ||
Theorem | elwspths2spth 27674* | A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = 〈“𝑎𝑏𝑐”〉 ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) | ||
Theorem | rusgrnumwwlkl1 27675* | In a k-regular graph, there are k walks (as word) of length 1 starting at each vertex. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = 𝐾) | ||
Theorem | rusgrnumwwlkslem 27676* | Lemma for rusgrnumwwlks 27681. (Contributed by Alexander van der Vekens, 23-Aug-2018.) |
⊢ (𝑌 ∈ {𝑤 ∈ 𝑍 ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ 𝜓)} = {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ (𝑌‘0) = 𝑃 ∧ 𝜓)}) | ||
Theorem | rusgrnumwwlklem 27677* | Lemma for rusgrnumwwlk 27682 etc. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃})) | ||
Theorem | rusgrnumwwlkb0 27678* | Induction base 0 for rusgrnumwwlk 27682. Here, we do not need the regularity of the graph yet. (Contributed by Alexander van der Vekens, 24-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) | ||
Theorem | rusgrnumwwlkb1 27679* | Induction base 1 for rusgrnumwwlk 27682. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿1) = 𝐾) | ||
Theorem | rusgr0edg 27680* | Special case for 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺 RegUSGraph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑃𝐿𝑁) = 0) | ||
Theorem | rusgrnumwwlks 27681* | Induction step for rusgrnumwwlk 27682. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) (Proof shortened by AV, 27-May-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))) | ||
Theorem | rusgrnumwwlk 27682* |
In a 𝐾-regular graph, the number of walks
of a fixed length 𝑁
from a fixed vertex is 𝐾 to the power of 𝑁. By
definition,
(𝑁
WWalksN 𝐺) is the
set of walks (as words) with length 𝑁,
and (𝑃𝐿𝑁) is the number of walks with length
𝑁
starting at
the vertex 𝑃. Because of the 𝐾-regularity, a walk can be
continued in 𝐾 different ways at the end vertex of
the walk, and
this repeated 𝑁 times.
This theorem even holds for 𝑁 = 0: in this case, the walk consists of only one vertex 𝑃, so the number of walks of length 𝑁 = 0 starting with 𝑃 is (𝐾↑0) = 1. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑃𝐿𝑁) = (𝐾↑𝑁)) | ||
Theorem | rusgrnumwwlkg 27683* | In a 𝐾-regular graph, the number of walks (as words) of a fixed length 𝑁 from a fixed vertex is 𝐾 to the power of 𝑁. Closed form of rusgrnumwwlk 27682. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) | ||
Theorem | rusgrnumwlkg 27684* | In a k-regular graph, the number of walks of a fixed length n from a fixed vertex is k to the power of n. This theorem corresponds to statement 11 in [Huneke] p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular." This theorem even holds for n=0: then the walk consists of only one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) (Proof shortened by AV, 5-Aug-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (♯‘{𝑤 ∈ (Walks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃)}) = (𝐾↑𝑁)) | ||
Theorem | clwwlknclwwlkdif 27685* | The set 𝐴 of walks of length 𝑁 starting with a fixed vertex 𝑉 and ending not at this vertex is the difference between the set 𝐶 of walks of length 𝑁 starting with this vertex 𝑋 and the set 𝐵 of closed walks of length 𝑁 anchored at this vertex 𝑋. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) (Revised by AV, 16-Mar-2022.) |
⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} & ⊢ 𝐵 = (𝑋(𝑁 WWalksNOn 𝐺)𝑋) & ⊢ 𝐶 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ⇒ ⊢ 𝐴 = (𝐶 ∖ 𝐵) | ||
Theorem | clwwlknclwwlkdifnum 27686* | In a 𝐾-regular graph, the size of the set 𝐴 of walks of length 𝑁 starting with a fixed vertex 𝑋 and ending not at this vertex is the difference between 𝐾 to the power of 𝑁 and the size of the set 𝐵 of closed walks of length 𝑁 anchored at this vertex 𝑋. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) (Revised by AV, 8-Mar-2022.) (Proof shortened by AV, 16-Mar-2022.) |
⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} & ⊢ 𝐵 = (𝑋(𝑁 WWalksNOn 𝐺)𝑋) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (♯‘𝐴) = ((𝐾↑𝑁) − (♯‘𝐵))) | ||
In general, a closed walk is an alternating sequence of vertices and edges, as defined in df-clwlks 27480: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n), with p(n) = p(0). Often, it is sufficient to refer to a walk by the (cyclic) sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(0), see the corresponding remark on cycles (which are special closed walks) in [Diestel] p. 7. As for "walks as words" in general, the concept of a Word, see df-word 13852, is also used in definitions df-clwwlk 27688 and df-clwwlkn 27731, and the representation of a closed walk as the sequence of its vertices is called "closed walk as word". In contrast to "walks as words", the terminating vertex p(n) of a closed walk is omitted in the representation of a closed walk as word, see definitions df-clwwlk 27688, df-clwwlkn 27731 and df-clwwlknon 27795, because it is always equal to the first vertex of the closed walk. This represenation has the advantage that the vertices can be cyclically shifted without changing the represented closed walk. Furthermore, the length of a closed walk (i.e. the number of its edges) equals the number of symbols/vertices of the word representing the closed walk. To avoid to handle the degenerate case of representing a (closed) walk of length 0 by the empty word, this case is excluded within the definition (𝑤 ≠ ∅). This is because a walk of length 0 is anchored at an arbitrary vertex by the general definition for closed walks, see 0clwlkv 27838, which neither can be reflected by the empty word nor by a singleton word 〈“𝑣”〉 with vertex v : 〈“𝑣”〉 represents the walk "𝑣 𝑣", which is a (closed) walk of length 1 (if there is an edge/loop from 𝑣 to 𝑣), see loopclwwlkn1b 27748. Therefore, a closed walk corresponds to a closed walk as word only for walks of length at least 1, see clwlkclwwlk2 27709 or clwlkclwwlken 27718. Although the set ClWWalksN of all closed walks of a fixed length as words over the set of vertices is defined as function over ℕ0, the fixed length is usually not 0, because (0 ClWWalksN 𝐺) = ∅ (see clwwlkn0 27734). Analogous to (𝐴(𝑁 WWalksNOn 𝐺)𝐵), the set of walks of a fixed length 𝑁 between two vertices 𝐴 and 𝐵, the set (𝑋(ClWWalksNOn‘𝐺)𝑁) of closed walks of a fixed length 𝑁 anchored at a fixed vertex 𝑋 is defined by df-clwwlknon 27795. This definition is also based on ℕ0 instead of ℕ, with (𝑋(ClWWalksNOn‘𝐺)0) = ∅ (see clwwlk0on0 27799). clwwlknon1le1 27808 states that there is at most one (closed) walk of length 1 on a vertex, which would consist of a loop (see clwwlknon1loop 27805). And in a 𝐾-regular graph, there are 𝐾 closed walks of length 2 on each vertex, see clwwlknon2num 27812. | ||
Syntax | cclwwlk 27687 | Extend class notation with closed walks (in an undirected graph) as word over the set of vertices. |
class ClWWalks | ||
Definition | df-clwwlk 27688* | Define the set of all closed walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 27480. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}) | ||
Theorem | clwwlk 27689* | The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (ClWWalks‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ 𝐸)} | ||
Theorem | isclwwlk 27690* | Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸)) | ||
Theorem | clwwlkbp 27691 | Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) | ||
Theorem | clwwlkgt0 27692 | There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → 0 < (♯‘𝑊)) | ||
Theorem | clwwlksswrd 27693 | Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) |
⊢ (ClWWalks‘𝐺) ⊆ Word (Vtx‘𝐺) | ||
Theorem | clwwlk1loop 27694 | A closed walk of length 1 is a loop. See also clwlkl1loop 27492. (Contributed by AV, 24-Apr-2021.) |
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ (♯‘𝑊) = 1) → {(𝑊‘0), (𝑊‘0)} ∈ (Edg‘𝐺)) | ||
Theorem | clwwlkccatlem 27695* | Lemma for clwwlkccat 27696: index 𝑗 is shifted up by (♯‘𝐴), and the case 𝑖 = ((♯‘𝐴) − 1) is covered by the "bridge" {(lastS‘𝐴), (𝐵‘0)} = {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺). (Contributed by AV, 23-Apr-2022.) |
⊢ ((((𝐴 ∈ Word (Vtx‘𝐺) ∧ 𝐴 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐴‘𝑖), (𝐴‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐴), (𝐴‘0)} ∈ (Edg‘𝐺)) ∧ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝐵 ≠ ∅) ∧ ∀𝑗 ∈ (0..^((♯‘𝐵) − 1)){(𝐵‘𝑗), (𝐵‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝐵), (𝐵‘0)} ∈ (Edg‘𝐺)) ∧ (𝐴‘0) = (𝐵‘0)) → ∀𝑖 ∈ (0..^((♯‘(𝐴 ++ 𝐵)) − 1)){((𝐴 ++ 𝐵)‘𝑖), ((𝐴 ++ 𝐵)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | ||
Theorem | clwwlkccat 27696 | The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022.) |
⊢ ((𝐴 ∈ (ClWWalks‘𝐺) ∧ 𝐵 ∈ (ClWWalks‘𝐺) ∧ (𝐴‘0) = (𝐵‘0)) → (𝐴 ++ 𝐵) ∈ (ClWWalks‘𝐺)) | ||
Theorem | umgrclwwlkge2 27697 | A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ (𝐺 ∈ UMGraph → (𝑃 ∈ (ClWWalks‘𝐺) → 2 ≤ (♯‘𝑃))) | ||
Theorem | clwlkclwwlklem2a1 27698* | Lemma 1 for clwlkclwwlklem2a 27704. (Contributed by Alexander van der Vekens, 21-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((♯‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | ||
Theorem | clwlkclwwlklem2a2 27699* | Lemma 2 for clwlkclwwlklem2a 27704. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ if(𝑥 < ((♯‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝐹) = ((♯‘𝑃) − 1)) | ||
Theorem | clwlkclwwlklem2a3 27700* | Lemma 3 for clwlkclwwlklem2a 27704. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((♯‘𝑃) − 1)) ↦ if(𝑥 < ((♯‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃‘(♯‘𝐹)) = (lastS‘𝑃)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |