![]() |
Metamath
Proof Explorer Theorem List (p. 273 of 435) | < 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-28329) |
![]() (28330-29854) |
![]() (29855-43446) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wwlksnred 27201 | 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 | wwlksnredOLD 27202 | Obsolete version of wwlksnred 27201 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wwlksnext 27203 | 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 27204 | 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 | wwlksnextbiOLD 27205 | Obsolete proof of wwlksnextbi 27204 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ 〈“𝑆”〉) ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ 𝑇 ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | wwlksnredwwlkn 27206* | 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 | wwlksnredwwlknOLD 27207* | Obsolete version of wwlksnredwwlkn 27206 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸))) | ||
Theorem | wwlksnredwwlkn0 27208* | 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 | wwlksnredwwlkn0OLD 27209* | Obsolete version of wwlksnredwwlkn0 27208 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑊)} ∈ 𝐸))) | ||
Theorem | wwlksnextwrd 27210* | Lemma for wwlksnextbij 27220. (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 27211* | Lemma for wwlksnextbij 27220. (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 27212* | Lemma for wwlksnextbij 27220. (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 27213* | Lemma for wwlksnextbij 27220. (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 27214* | Lemma for wwlksnextbij 27220. (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 | wwlksnextwrdOLD 27215* | Obsolete version of wwlksnextwrd 27210 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐷 = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) | ||
Theorem | wwlksnextfunOLD 27216* | Obsolete version of wwlksnextfun 27211 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷⟶𝑅) | ||
Theorem | wwlksnextinjOLD 27217* | Obsolete version of wwlksnextinj 27212 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷–1-1→𝑅) | ||
Theorem | wwlksnextsurOLD 27218* | Obsolete version of wwlksnextsurj 27213 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–onto→𝑅) | ||
Theorem | wwlksnextbij0OLD 27219* | Obsolete version of wwlksnextbij0 27214 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (lastS‘𝑡)) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝐹:𝐷–1-1-onto→𝑅) | ||
Theorem | wwlksnextbij 27220* | 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 | wwlksnextbijOLD 27221* | Obsolete version of wwlksnextbij 27220 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 18-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸}) | ||
Theorem | wwlksnexthasheq 27222* | 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 | wwlksnexthasheqOLD 27223* | Obsolete version of wwlksnexthasheq 27222 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Proof shortened by AV, 5-May-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {(lastS‘𝑊), (lastS‘𝑤)} ∈ 𝐸)}) = (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑊), 𝑛} ∈ 𝐸})) | ||
Theorem | disjxwwlksn 27224* | 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 | disjxwwlksnOLD 27225* | Obsolete version of disjxwwlksn 27224 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 29-Jul-2018.) (Revised by AV, 19-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ Disj 𝑦 ∈ (𝑁 WWalksN 𝐺){𝑥 ∈ Word 𝑉 ∣ ((𝑥 substr 〈0, 𝑁〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} | ||
Theorem | wwlksnndef 27226 | 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 27227 | 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.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin) | ||
Theorem | wlksnfi 27228* | 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 27229* | 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 | wlksnwwlknvbijOLD 27230* | Obsolete version of wlksnwwlknvbij 27229 as of 5-Aug-2022. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ (Vtx‘𝐺)) → ∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) | ||
Theorem | wwlksnextproplem1 27231 | Lemma 1 for wwlksnextprop 27237. (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 | wwlksnextproplem1OLD 27232 | Obsolete version of wwlksnextproplem1 27231 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 31-Jul-2018.) (Revised by AV, 20-Apr-2021.) (Proof shortened by AV, 13-Mar-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) | ||
Theorem | wwlksnextproplem2 27233 | Lemma 2 for wwlksnextprop 27237. (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 | wwlksnextproplem2OLD 27234 | Obsolete version of wwlksnextproplem2 27233 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {(lastS‘(𝑊 substr 〈0, (𝑁 + 1)〉)), (lastS‘𝑊)} ∈ 𝐸) | ||
Theorem | wwlksnextproplem3 27235* | Lemma 3 for wwlksnextprop 27237. (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 | wwlksnextproplem3OLD 27236* | Obsolete version of wwlksnextproplem3 27235 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) | ||
Theorem | wwlksnextprop 27237* | 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 | wwlksnextpropOLD 27238* | Obsolete version of wwlksnextprop 27237 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ (𝑁 ∈ ℕ0 → {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) | ||
Theorem | disjxwwlkn 27239* | 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 | disjxwwlknOLD 27240* | Obsolete version of disjxwwlkn 27239 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)} | ||
Theorem | hashwwlksnext 27241* | 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 | hashwwlksnextOLD 27242* | Obsolete version of hashwwlksnext 27241 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) = Σ𝑦 ∈ 𝑌 (♯‘{𝑥 ∈ 𝑋 ∣ ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)})) | ||
Theorem | wwlksnwwlksnon 27243* | 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 27244* | 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 27245 | 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 27246 | 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 27247 | 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 27248 | 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 27249 | 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 27250 | 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 27251* | 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 27252 | 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 27253 | Lemma 1 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1) | ||
Theorem | 2wlkdlem2 27254 | Lemma 2 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 ⇒ ⊢ (0..^(♯‘𝐹)) = {0, 1} | ||
Theorem | 2wlkdlem3 27255 | Lemma 3 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵 ∧ (𝑃‘2) = 𝐶)) | ||
Theorem | 2wlkdlem4 27256* | Lemma 4 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) | ||
Theorem | 2wlkdlem5 27257* | Lemma 5 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 2pthdlem1 27258* | Lemma 1 for 2pthd 27268. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗))) | ||
Theorem | 2wlkdlem6 27259 | Lemma 6 for 2wlkd 27264. (Contributed by AV, 23-Jan-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐵 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾))) | ||
Theorem | 2wlkdlem7 27260 | Lemma 7 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V)) | ||
Theorem | 2wlkdlem8 27261 | Lemma 8 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾)) | ||
Theorem | 2wlkdlem9 27262 | Lemma 9 for 2wlkd 27264. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)))) | ||
Theorem | 2wlkdlem10 27263* | Lemma 10 for 3wlkd 27545. (Contributed by AV, 14-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶”〉 & ⊢ 𝐹 = 〈“𝐽𝐾”〉 & ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 2wlkd 27264 | 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 27265 | 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 27266 | 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 27267 | 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 27268 | 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 27269 | 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 27270 | 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 27271* | 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 27272 | Lemma for umgr2adedgwlk 27273, umgr2adedgspth 27276, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ∧ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺) ∧ 𝐶 ∈ (Vtx‘𝐺)))) | ||
Theorem | umgr2adedgwlk 27273 | 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 27274 | 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 27275 | Alternate proof for umgr2adedgwlkon 27274, using umgr2adedgwlk 27273, 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 27276 | 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 27277* | 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 27278* | 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 27279* | A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (2 WWalksN 𝐺) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) | ||
Theorem | midwwlks2s3 27280* | 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 27281 | 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 27282 | 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 27283* | 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 27284* | 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 27285 | 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 27286 | 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 27287* | 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 27288* | 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 27289 | 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 27290* | 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 27291* | 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 27292 | 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 27293* | 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 27294* | 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 27295* | 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 27296* | 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 27297* | Lemma for rusgrnumwwlks 27302. (Contributed by Alexander van der Vekens, 23-Aug-2018.) |
⊢ (𝑌 ∈ {𝑤 ∈ 𝑍 ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ 𝜓)} = {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ (𝑌‘0) = 𝑃 ∧ 𝜓)}) | ||
Theorem | rusgrnumwwlklem 27298* | Lemma for rusgrnumwwlk 27304 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 27299* | Induction base 0 for rusgrnumwwlk 27304. 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 27300* | Induction base 1 for rusgrnumwwlk 27304. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) ⇒ ⊢ ((𝐺RegUSGraph𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿1) = 𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |