P. 281 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28001-28100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgr2pthnlp 28001*	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 28002	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 28003	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 28004	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 28005*	Lemma for upgrwlkdvde 28006. (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 28006	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 28007. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹)
Theorem	upgrspthswlk 28007*	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 28008	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 28007. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	pthsonfval 28009*	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 28010*	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 28011	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 28012	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 28013	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 28014	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 28015	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 28016	A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃)
Theorem	pthonpth 28017	A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
Theorem	isspthonpth 28018	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 28019	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 28020	A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃)
Theorem	spthonepeq 28021	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 28022	Lemma 1 for uhgrwkspth 28024. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹)
Theorem	uhgrwkspthlem2 28023	Lemma 2 for uhgrwkspth 28024. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃)
Theorem	uhgrwkspth 28024	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 28025	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 28026	Lemma 1 for usgr2wlkspth 28028. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹)
Theorem	usgr2wlkspthlem2 28027	Lemma 2 for usgr2wlkspth 28028. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃)
Theorem	usgr2wlkspth 28028	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 28029	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 28030	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 28031	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 28032*	Lemma for usgr2pth 28033. (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 28033*	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 28034*	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 28035*	Lemma 1 for pthd 28038. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅)))
Theorem	pthdlem2lem 28036*	Lemma for pthdlem2 28037. (Contributed by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)))
Theorem	pthdlem2 28037*	Lemma 2 for pthd 28038. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)
Theorem	pthd 28038*	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‘𝐺)𝑃)
16.3.5  Closed walks
Syntax	cclwlks 28039	Extend class notation with closed walks (of a graph).
class ClWalks
Definition	df-clwlks 28040*	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 28395. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.)
⊢ ClWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))})
Theorem	clwlks 28041*	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 28042	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 28043	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 28044	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 28045	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 28046*	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 28047*	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 28048*	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 28049*	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 28050*	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 28051	Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.)
⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (ClWalks‘𝐺) → (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
Theorem	clwlkl1loop 28052	A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.)
⊢ ((Fun (iEdg‘𝐺) ∧ 𝐹(ClWalks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → ((𝑃‘0) = (𝑃‘1) ∧ {(𝑃‘0)} ∈ (Edg‘𝐺)))
16.3.6  Circuits and cycles
Syntax	ccrcts 28053	Extend class notation with circuits (in a graph).
class Circuits
Syntax	ccycls 28054	Extend class notation with cycles (in a graph).
class Cycles
Definition	df-crcts 28055*	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 28056*	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 28057*	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 28058*	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 28059	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 28060	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 28061	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 28062	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 28063	A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(ClWalks‘𝐺)𝑃)
Theorem	crctistrl 28064	A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	crctiswlk 28065	A circuit is a walk. (Contributed by AV, 6-Apr-2021.)
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	cyclispth 28066	A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	cycliswlk 28067	A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.)
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	cycliscrct 28068	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	cyclnspth 28069	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	cyclispthon 28070	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 28071*	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 28072	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 28073	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 28074	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 28075	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 28076	Lemma for crctcshwlkn0 28087. (Contributed by AV, 13-Mar-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → ((𝐴 − 𝐵) + 1) ≤ 𝐴)
Theorem	crctcshwlkn0lem2 28077*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ (0...(𝑁 − 𝑆))) → (𝑄‘𝐽) = (𝑃‘(𝐽 + 𝑆)))
Theorem	crctcshwlkn0lem3 28078*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘𝐽) = (𝑃‘((𝐽 + 𝑆) − 𝑁)))
Theorem	crctcshwlkn0lem4 28079*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    ⇒   ⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
Theorem	crctcshwlkn0lem5 28080*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    ⇒   ⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
Theorem	crctcshwlkn0lem6 28081*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))    ⇒   ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))
Theorem	crctcshwlkn0lem7 28082*	Lemma for crctcshwlkn0 28087. (Contributed by AV, 12-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))    ⇒   ⊢ (𝜑 → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
Theorem	crctcshlem1 28083	Lemma for crctcsh 28090. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	crctcshlem2 28084	Lemma for crctcsh 28090. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    ⇒   ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
Theorem	crctcshlem3 28085*	Lemma for crctcsh 28090. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
Theorem	crctcshlem4 28086*	Lemma for crctcsh 28090. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐻 = 𝐹 ∧ 𝑄 = 𝑃))
Theorem	crctcshwlkn0 28087*	Cyclically shifting the indices of a circuit ⟨𝐹, 𝑃⟩ results in a walk ⟨𝐻, 𝑄⟩. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)
Theorem	crctcshwlk 28088*	Cyclically shifting the indices of a circuit ⟨𝐹, 𝑃⟩ results in a walk ⟨𝐻, 𝑄⟩. (Contributed by AV, 10-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ (𝜑 → 𝐻(Walks‘𝐺)𝑄)
Theorem	crctcshtrl 28089*	Cyclically shifting the indices of a circuit ⟨𝐹, 𝑃⟩ results in a trail ⟨𝐻, 𝑄⟩. (Contributed by AV, 14-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ (𝜑 → 𝐻(Trails‘𝐺)𝑄)
Theorem	crctcsh 28090*	Cyclically shifting the indices of a circuit ⟨𝐹, 𝑃⟩ results in a circuit ⟨𝐻, 𝑄⟩. (Contributed by AV, 10-Mar-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    ⇒   ⊢ (𝜑 → 𝐻(Circuits‘𝐺)𝑄)
16.3.7  Walks as words In general, a walk is an alternating sequence of vertices and edges, as defined in df-wlks 27869: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14146, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in Definitions df-wwlks 28096 and df-wwlksn 28097, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph).
Syntax	cwwlks 28091	Extend class notation with walks (in a graph) as word over the set of vertices.
class WWalks
Syntax	cwwlksn 28092	Extend class notation with walks (in a graph) of a fixed length as word over the set of vertices.
class WWalksN
Syntax	cwwlksnon 28093	Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WWalksNOn
Syntax	cwwspthsn 28094	Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices.
class WSPathsN
Syntax	cwwspthsnon 28095	Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices.
class WSPathsNOn
Definition	df-wwlks 28096*	Define the set of all 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) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 27869. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 27890. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ WWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))})
Definition	df-wwlksn 28097*	Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 27869. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)
⊢ WWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})
Definition	df-wwlksnon 28098*	Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)
⊢ WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))
Definition	df-wspthsn 28099*	Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})
Definition	df-wspthsnon 28100*	Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
⊢ WSPathsNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}))