P. 299 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29801-29900   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-pthson 29801*	Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ PathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)}))
Definition	df-spthson 29802*	Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.)
⊢ SPathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPaths‘𝑔)𝑝)}))
Theorem	relpths 29803	The set (Paths‘𝐺) of all paths on 𝐺 is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.)
⊢ Rel (Paths‘𝐺)
Theorem	pthsfval 29804*	The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (Paths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)}
Theorem	spthsfval 29805*	The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡𝑝)}
Theorem	ispth 29806	Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
Theorem	isspth 29807	Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃))
Theorem	pthistrl 29808	A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	spthispth 29809	A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthiswlk 29810	A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	spthiswlk 29811	A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	pthdivtx 29812	The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(♯‘𝐹)) ∧ 𝐽 ∈ (0...(♯‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))
Theorem	pthdadjvtx 29813	The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 𝐼 ∈ (0..^(♯‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1)))
Theorem	dfpth2 29814	Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
Theorem	pthdifv 29815	The vertices of a path are distinct (except the first and last vertex), so the restricted vertex function is one-to-one. (Contributed by AV, 2-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	2pthnloop 29816*	A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 30238. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖))))
Theorem	upgr2pthnlp 29817*	A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))(♯‘(𝐼‘(𝐹‘𝑖))) = 2)
Theorem	spthdifv 29818	The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	spthdep 29819	A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(SPaths‘𝐺)𝑃 ∧ (♯‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))
Theorem	pthdepisspth 29820	A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	upgrwlkdvdelem 29821*	Lemma for upgrwlkdvde 29822. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.)
⊢ ((𝑃:(0...(♯‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))
Theorem	upgrwlkdvde 29822	In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29823. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹)
Theorem	upgrspthswlk 29823*	The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐺 ∈ UPGraph → (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)})
Theorem	upgrwlkdvspth 29824	A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29823. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	pthsonfval 29825*	The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(PathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Paths‘𝐺)𝑝)})
Theorem	spthson 29826*	The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(SPathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(SPaths‘𝐺)𝑝)})
Theorem	ispthson 29827	Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	isspthson 29828	Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthsonprop 29829	Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	spthonprop 29830	Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthonispth 29831	A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthontrlon 29832	A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃)
Theorem	pthonpth 29833	A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
Theorem	isspthonpth 29834	A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)))
Theorem	spthonisspth 29835	A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(SPaths‘𝐺)𝑃)
Theorem	spthonpthon 29836	A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃)
Theorem	spthonepeq 29837	The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (♯‘𝐹) = 0))
Theorem	uhgrwkspthlem1 29838	Lemma 1 for uhgrwkspth 29840. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹)
Theorem	uhgrwkspthlem2 29839	Lemma 2 for uhgrwkspth 29840. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃)
Theorem	uhgrwkspth 29840	Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.)
⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2wlkneq 29841	The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))
Theorem	usgr2wlkspthlem1 29842	Lemma 1 for usgr2wlkspth 29844. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹)
Theorem	usgr2wlkspthlem2 29843	Lemma 2 for usgr2wlkspth 29844. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃)
Theorem	usgr2wlkspth 29844	In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2trlncl 29845	In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))
Theorem	usgr2trlspth 29846	In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthspth 29847	In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Paths‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthlem 29848*	Lemma for usgr2pth 29849. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
Theorem	usgr2pth 29849*	In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))
Theorem	usgr2pth0 29850*	In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦})))))
Theorem	pthdlem1 29851*	Lemma 1 for pthd 29854. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅)))
Theorem	pthdlem2lem 29852*	Lemma for pthdlem2 29853. (Contributed by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)))
Theorem	pthdlem2 29853*	Lemma 2 for pthd 29854. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)
Theorem	pthd 29854*	Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    &   ⊢ (♯‘𝐹) = 𝑅    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
17.3.5  Closed walks
Syntax	cclwlks 29855	Extend class notation with closed walks (of a graph).
class ClWalks
Definition	df-clwlks 29856*	Define the set of all closed walks (in an undirected graph). According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex can be considered as a closed walk of length 0, see also 0clwlk 30217. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.)
⊢ ClWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))})
Theorem	clwlks 29857*	The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (ClWalks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}
Theorem	isclwlk 29858	A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(ClWalks‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	clwlkiswlk 29859	A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(ClWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	clwlkwlk 29860	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝑊 ∈ (ClWalks‘𝐺) → 𝑊 ∈ (Walks‘𝐺))
Theorem	clwlkswks 29861	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.)
⊢ (ClWalks‘𝐺) ⊆ (Walks‘𝐺)
Theorem	isclwlke 29862*	Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑋 → (𝐹(ClWalks‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))))
Theorem	isclwlkupgr 29863*	Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 11-Apr-2021.) (Revised by AV, 28-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(ClWalks‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))))
Theorem	clwlkcomp 29864*	A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ ((𝐺 ∈ 𝑋 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (ClWalks‘𝐺) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))))
Theorem	clwlkcompim 29865*	Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (ClWalks‘𝐺) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))
Theorem	upgrclwlkcompim 29866*	Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 2-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (ClWalks‘𝐺)) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	clwlkcompbp 29867	Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.)
⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (ClWalks‘𝐺) → (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	clwlkl1loop 29868	A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.)
⊢ ((Fun (iEdg‘𝐺) ∧ 𝐹(ClWalks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → ((𝑃‘0) = (𝑃‘1) ∧ {(𝑃‘0)} ∈ (Edg‘𝐺)))
17.3.6  Circuits and cycles
Syntax	ccrcts 29869	Extend class notation with circuits (in a graph).
class Circuits
Syntax	ccycls 29870	Extend class notation with cycles (in a graph).
class Cycles
Definition	df-crcts 29871*	Define the set of all circuits (in an undirected graph). According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...". Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of [Bollobas] p. 5.), a circuit is a closed trail without repeated edges. So the circuit is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ Circuits = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))})
Definition	df-cycls 29872*	Define the set of all (simple) cycles (in an undirected graph). According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex." According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of [Bollobas] p. 5. However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ Cycles = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Paths‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))})
Theorem	crcts 29873*	The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (Circuits‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}
Theorem	cycls 29874*	The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (Cycles‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}
Theorem	iscrct 29875	Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	iscycl 29876	Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	crctprop 29877	The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	cyclprop 29878	The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	crctisclwlk 29879	A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(ClWalks‘𝐺)𝑃)
Theorem	crctistrl 29880	A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	crctiswlk 29881	A circuit is a walk. (Contributed by AV, 6-Apr-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	cyclispth 29882	A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	cycliswlk 29883	A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	cycliscrct 29884	A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Circuits‘𝐺)𝑃)
Theorem	cyclnumvtx 29885	The number of vertices of a (non-trivial) cycle is the number of edges in the cycle. (Contributed by AV, 5-Oct-2025.)
⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘ran 𝑃) = (♯‘𝐹))
Theorem	cyclnspth 29886	A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃))
Theorem	pthisspthorcycl 29887	A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃))
Theorem	pthspthcyc 29888	A pair ⟨𝐹, 𝑃⟩ represents a path if it represents either a simple path or a cycle. The exclusivity only holds for non-trivial paths (𝐹 ≠ ∅), see cyclnspth 29886. (Contributed by AV, 2-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃))
Theorem	cyclispthon 29889	A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘0))𝑃)
Theorem	lfgrn1cycl 29890*	In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ≠ 1))
Theorem	usgr2trlncrct 29891	In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → ¬ 𝐹(Circuits‘𝐺)𝑃))
Theorem	umgrn1cycl 29892	In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 1)
Theorem	uspgrn2crct 29893	In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 3-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹(Circuits‘𝐺)𝑃) → (♯‘𝐹) ≠ 2)
Theorem	usgrn2cycl 29894	In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 4-Feb-2021.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 2)
Theorem	crctcshwlkn0lem1 29895	Lemma for crctcshwlkn0 29906. (Contributed by AV, 13-Mar-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → ((𝐴 − 𝐵) + 1) ≤ 𝐴)
Theorem	crctcshwlkn0lem2 29896*	Lemma for crctcshwlkn0 29906. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ (0...(𝑁 − 𝑆))) → (𝑄‘𝐽) = (𝑃‘(𝐽 + 𝑆)))
Theorem	crctcshwlkn0lem3 29897*	Lemma for crctcshwlkn0 29906. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘𝐽) = (𝑃‘((𝐽 + 𝑆) − 𝑁)))
Theorem	crctcshwlkn0lem4 29898*	Lemma for crctcshwlkn0 29906. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    ⇒   ⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
Theorem	crctcshwlkn0lem5 29899*	Lemma for crctcshwlkn0 29906. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    ⇒   ⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
Theorem	crctcshwlkn0lem6 29900*	Lemma for crctcshwlkn0 29906. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))    ⇒   ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))