P. 263 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26201-26300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isconngra1 26201*	The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ConnGrph 𝐸 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝))
Theorem	0conngra 26202	A class/graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
⊢ (𝐸 ∈ 𝑉 → ∅ ConnGrph 𝐸)
Theorem	1conngra 26203	A class/graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.)
⊢ (𝐸 ∈ 𝑉 → {𝐴} ConnGrph 𝐸)
Theorem	cusconngra 26204	A complete (undirected simple) graph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 ConnGrph 𝐸)
17.1.5.5  Walks as words
Syntax	cwwlk 26205	Extend class notation with Walks (of a graph) as Word over the set of vertices.
class WWalks
Syntax	cwwlkn 26206	Extend class notation with Walks (of a graph) of a fixed length as Word over the set of vertices.
class WWalksN
Definition	df-wwlk 26207*	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-wlk 26036. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26055. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})
Definition	df-wwlkn 26208*	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-wlk 26036. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ WWalksN = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)}))
Theorem	wwlk 26209*	The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 WWalks 𝐸) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)})
Theorem	wwlkn 26210*	The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 WWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (𝑁 + 1)})
Theorem	iswwlk 26211*	Properties of a word to represent a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑊 ∈ (𝑉 WWalks 𝐸) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)))
Theorem	iswwlkn 26212	Properties of a word to represent a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1))))
Theorem	wwlkprop 26213	Properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))
Theorem	wwlknprop 26214	Properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.)
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word 𝑉)))
Theorem	wwlknimp 26215*	Implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.)
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))
Theorem	wwlksswrd 26216	Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
⊢ (𝑉 WWalks 𝐸) ⊆ Word 𝑉
Theorem	wwlkn0 26217*	A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘0) → ∃𝑣 ∈ 𝑉 𝑊 = ⟨“𝑣”⟩)
Theorem	wlkiswwlk1 26218	The sequence of vertices in a walk is a walk as word in an undirected simple graph. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ∈ (𝑉 WWalks 𝐸)))
Theorem	wlkiswwlk2lem1 26219*	Lemma 1 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1))
Theorem	wlkiswwlk2lem2 26220*	Lemma 2 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))
Theorem	wlkiswwlk2lem3 26221*	Lemma 3 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝑃:(0...(#‘𝐹))⟶𝑉)
Theorem	wlkiswwlk2lem4 26222*	Lemma 4 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))
Theorem	wlkiswwlk2lem5 26223*	Lemma 5 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸))
Theorem	wlkiswwlk2lem6 26224*	Lemma 6 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})))
Theorem	wlkiswwlk2 26225*	A walk as word corresponds to the sequence of vertices in a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 WWalks 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃))
Theorem	wlkiswwlk 26226*	A walk as word corresponds to a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃 ↔ 𝑃 ∈ (𝑉 WWalks 𝐸)))
Theorem	wlklniswwlkn1 26227	The sequence of vertices in a walk of length n is a walk as word of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))
Theorem	wlklniswwlkn2 26228*	A walk of length n as word corresponds to the sequence of vertices in a walk of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁)))
Theorem	wlklniswwlkn 26229*	A walk of length n as word corresponds to a walk with length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
⊢ (𝑉 USGrph 𝐸 → (∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁) ↔ 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))
Theorem	wwlkiswwlkn 26230	A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝑃 ∈ (𝑉 WWalks 𝐸))
Theorem	wwlksswwlkn 26231	The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.)
⊢ ((𝑉 WWalksN 𝐸)‘𝑁) ⊆ (𝑉 WWalks 𝐸)
Theorem	wwlknimpb 26232	Basic implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 3-Oct-2018.)
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1)))
Theorem	wwlkn0s 26233*	The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1})
Theorem	vfwlkniswwlkn 26234	If the edge function of a walk has length n, then the vertex function of the walk is a word representing the walk as word of length n. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))
Theorem	2wlkeq 26235*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.)
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))
Theorem	usg2wlkeq 26236*	Conditions for two walks within the same undirected simple graph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦))))
Theorem	usg2wlkeq2 26237	Conditions for which two walks within the same undirected simple graph are the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑋) = (2nd ‘𝑊) → 𝑋 = 𝑊))
Theorem	wlknwwlknfun 26238*	Lemma 1 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}    &   ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑇⟶𝑊)
Theorem	wlknwwlkninj 26239*	Lemma 2 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}    &   ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊)
Theorem	wlknwwlknsur 26240*	Lemma 3 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}    &   ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊)
Theorem	wlknwwlknbij 26241*	Lemma 4 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}    &   ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊)
Theorem	wlknwwlknbij2 26242*	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. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}–1-1-onto→((𝑉 WWalksN 𝐸)‘𝑁))
Theorem	wlknwwlknen 26243*	The set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} ≈ ((𝑉 WWalksN 𝐸)‘𝑁))
Theorem	wlknwwlkneqs 26244*	The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (#‘{𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}) = (#‘((𝑉 WWalksN 𝐸)‘𝑁)))
Theorem	wlkiswwlkfun 26245*	Lemma 1 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}    &   ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊)
Theorem	wlkiswwlkinj 26246*	Lemma 2 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}    &   ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊)
Theorem	wlkiswwlksur 26247*	Lemma 3 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 23-Jul-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}    &   ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊)
Theorem	wlkiswwlkbij 26248*	Lemma 4 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}    &   ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡))    ⇒   ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊)
Theorem	wlkiswwlkbij2 26249*	There is a bijection between the set of walks of a fixed length, starting at a fixed vertex, and the set of walks represented as words of the same length, starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})
Theorem	wwlkeq 26250*	Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.)
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 𝑇 ∈ (𝑉 WWalks 𝐸)) → (𝑊 = 𝑇 ↔ ((#‘𝑊) = (#‘𝑇) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑇‘𝑖))))
Theorem	wwlknred 26251	Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.)
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 substr ⟨0, (𝑁 + 1)⟩) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))
Theorem	wwlknext 26252	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.)
⊢ ((𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)))
Theorem	wwlknextbi 26253	Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ ⟨“𝑆”⟩) ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ 𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)))
Theorem	wwlknredwwlkn 26254*	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.)
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)))
Theorem	wwlknredwwlkn0 26255*	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.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸)))
Theorem	wwlkextwrd 26256*	Lemma 0 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 5-Aug-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}    ⇒   ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)})
Theorem	wwlkextfun 26257*	Lemma 1 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷⟶𝑅)
Theorem	wwlkextinj 26258*	Lemma 2 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷–1-1→𝑅)
Theorem	wwlkextsur 26259*	Lemma 3 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))    ⇒   ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷–onto→𝑅)
Theorem	wwlkextbij0 26260*	Lemma 4 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.)
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}    &   ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}    &   ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡))    ⇒   ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷–1-1-onto→𝑅)
Theorem	wwlkextbij 26261*	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.)
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸})
Theorem	wwlkexthasheq 26262*	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.) (Proof shortened by AV, 4-May-2021.)
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}))
Theorem	wwlkm1edg 26263	Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr ⟨0, ((#‘𝑊) − 1)⟩) ∈ (𝑉 WWalks 𝐸))
Theorem	disjxwwlks 26264*	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.)
⊢ Disj 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁){𝑥 ∈ Word 𝑉 ∣ ((𝑥 substr ⟨0, 𝑁⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}
Theorem	wwlknndef 26265	Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.)
⊢ ((𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0) → ((𝑉 WWalksN 𝐸)‘𝑁) = ∅)
Theorem	wwlknfi 26266	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.)
⊢ (𝑉 ∈ Fin → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin)
Theorem	wlknfi 26267*	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.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑉 ∈ Fin) → {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} ∈ Fin)
Theorem	wlknwwlknvbij 26268*	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, 30-Sep-2018.)
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋})
Theorem	wwlkextproplem1 26269	Lemma 1 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 31-Jul-2018.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr ⟨0, (𝑁 + 1)⟩)‘0) = (𝑊‘0))
Theorem	wwlkextproplem2 26270	Lemma 2 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {( lastS ‘(𝑊 substr ⟨0, (𝑁 + 1)⟩)), ( lastS ‘𝑊)} ∈ ran 𝐸)
Theorem	wwlkextproplem3 26271*	Lemma 3 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    &   ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 substr ⟨0, (𝑁 + 1)⟩) ∈ 𝑌)
Theorem	wwlkextprop 26272*	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.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    &   ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ (𝑁 ∈ ℕ0 → {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)})
Theorem	disjxwwlkn 26273*	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.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    &   ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ ((𝑥 substr ⟨0, 𝑀⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}
Theorem	hashwwlkext 26274*	Number of walks (as words) extended by an edge as sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.)
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))    &   ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}    ⇒   ⊢ (𝑉 ∈ Fin → (#‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr ⟨0, 𝑀⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}) = Σ𝑦 ∈ 𝑌 (#‘{𝑥 ∈ 𝑋 ∣ ((𝑥 substr ⟨0, 𝑀⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}))
17.1.5.6  Closed walks
Syntax	cclwlk 26275	Extend class notation with Closed Walks (of a graph).
class ClWalks
Syntax	cclwwlk 26276	Extend class notation with Closed Walks (of a graph) as Word over the set of vertices.
class ClWWalks
Syntax	cclwwlkn 26277	Extend class notation with Closed Walks (of a graph) of a fixed length as Word over the set of vertices.
class ClWWalksN
Definition	df-clwlk 26278*	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 { 1 , ... , n } 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(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). Notice that by this definition, a single vertex is a closed walk of length 0, see also 0clwlk 26293! (Contributed by Alexander van der Vekens, 12-Mar-2018.)
⊢ ClWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))})
Definition	df-clwwlk 26279*	Define the set of all Closed Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 26278. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. Notice that by this definition, a single vertex cannot be represented as closed walk, since the word <" v "> with vertex v represents the walk "vv", which is a (closed) walk of length 1 (if there is an edge/loop from v to v). Therefore, a closed walk corresponds to a closed walk as word in an undirected graph only for walks of length at least 1, see clwlkisclwwlk2 26318. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ ClWWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)})
Definition	df-clwwlkn 26280*	Define the set of all Closed 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-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 26278. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ ClWWalksN = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}))
Theorem	clwlk 26281*	The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWalks 𝐸) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))})
Theorem	isclwlk0 26282	Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
Theorem	isclwlkg 26283	Generalisation of isclwlk0 26282: Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
Theorem	isclwlk 26284*	Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))))
Theorem	clwlkiswlk 26285	A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ (𝐹(𝑉 ClWalks 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃)
Theorem	clwlkswlks 26286	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.)
⊢ (𝑊 ∈ (𝑉 ClWalks 𝐸) → 𝑊 ∈ (𝑉 Walks 𝐸))
Theorem	clwlksarewlks 26287	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.)
⊢ (𝑉 ClWalks 𝐸) ⊆ (𝑉 Walks 𝐸)
Theorem	wlkv0 26288	If there is a walk in an empty graph, it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
⊢ (𝑊 ∈ (∅ Walks 𝐸) → ((1st ‘𝑊) = ∅ ∧ (2nd ‘𝑊) = ∅))
Theorem	wlk0 26289	There is no walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
⊢ (∅ Walks 𝐸) = ∅
Theorem	clwlk0 26290	There is no closed walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
⊢ (∅ ClWalks 𝐸) = ∅
Theorem	clwlkcomp 26291*	A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (𝑉 ClWalks 𝐸) ↔ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))))
Theorem	clwlkcompim 26292*	Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (𝑉 ClWalks 𝐸) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
Theorem	0clwlk 26293	A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 ClWalks 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	clwwlk 26294*	The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWWalks 𝐸) = {𝑤 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸)})
Theorem	clwwlkn 26295*	The set of closed walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁})
Theorem	isclwwlk 26296*	Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)))
Theorem	isclwwlkn 26297	Properties of a word to represent a closed walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 𝑁)))
Theorem	clwwlkprop 26298	Properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉))
Theorem	clwwlkgt0 26299	A closed walk in an undirected graph has a length of at least 2. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))
Theorem	clwwlknprop 26300	Properties of a closed walk of a fixed length as word. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑃) = 𝑁)))