P. 308 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30701-30800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hashecclwwlkn1 30701*	The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝑁 ∈ ℙ ∧ 𝑈 ∈ (𝑊 / ∼ )) → ((♯‘𝑈) = 1 ∨ (♯‘𝑈) = 𝑁))
Theorem	umgrhashecclwwlk 30702*	The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number equals this length (in an undirected simple graph). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 ∈ (𝑊 / ∼ ) → (♯‘𝑈) = 𝑁))
Theorem	fusgrhashclwwlkn 30703*	The size of the set of closed walks (defined as words) with a fixed length which is a prime number is the product of the number of equivalence classes for ∼ over the set of closed walks and the fixed length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (♯‘𝑊) = ((♯‘(𝑊 / ∼ )) · 𝑁))
Theorem	clwwlkndivn 30704	The size of the set of closed walks (defined as words) of length 𝑁 is divisible by 𝑁 if 𝑁 is a prime number. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 2-May-2021.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (♯‘(𝑁 ClWWalksN 𝐺)))
Theorem	clwlknf1oclwwlknlem1 30705	Lemma 1 for clwlknf1oclwwlkn 30708. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝐶))) → (♯‘((2nd ‘𝐶) prefix ((♯‘(2nd ‘𝐶)) − 1))) = (♯‘(1st ‘𝐶)))
Theorem	clwlknf1oclwwlknlem2 30706*	Lemma 2 for clwlknf1oclwwlkn 30708: The closed walks of a positive length are nonempty closed walks of this length. (Contributed by AV, 26-May-2022.)
⊢ (𝑁 ∈ ℕ → {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)})
Theorem	clwlknf1oclwwlknlem3 30707*	Lemma 3 for clwlknf1oclwwlkn 30708: The bijective function of clwlknf1oclwwlkn 30708 is the bijective function of clwlkclwwlkf1o 30635 restricted to the closed walks with a fixed positive length. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ 𝐴 = (1st ‘𝑐)    &   ⊢ 𝐵 = (2nd ‘𝑐)    &   ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁}    &   ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 prefix (♯‘𝐴)))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ (𝐵 prefix (♯‘𝐴))) ↾ 𝐶))
Theorem	clwlknf1oclwwlkn 30708*	There is a one-to-one onto function between the set of closed walks as words of length 𝑁 and the set of closed walks of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 1-Nov-2022.)
⊢ 𝐴 = (1st ‘𝑐)    &   ⊢ 𝐵 = (2nd ‘𝑐)    &   ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁}    &   ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 prefix (♯‘𝐴)))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹:𝐶⟶1-1onto(𝑁 ClWWalksN 𝐺))
Theorem	clwlkssizeeq 30709*	The size of the set of closed walks as words of length 𝑁 corresponds to the size of the set of closed walks of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) (Revised by AV, 26-May-2022.) (Proof shortened by AV, 3-Nov-2022.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (♯‘(𝑁 ClWWalksN 𝐺)) = (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁}))
Theorem	clwlksndivn 30710*	The size of the set of closed walks of prime length 𝑁 is divisible by 𝑁. This corresponds to statement 9 in [Huneke] p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p". (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (♯‘{𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑐)) = 𝑁}))
17.3.10.3  Closed walks on a vertex of a fixed length as words
Syntax	cclwwlknon 30711	Extend class notation with closed walks (in an undirected graph) anchored at a fixed vertex and of a fixed length as word over the set of vertices.
class ClWWalksNOn
Definition	df-clwwlknon 30712*	Define the set of all closed walks a graph 𝑔, anchored at a fixed vertex 𝑣 (i.e., a walk starting and ending at the fixed vertex 𝑣, also called "a closed walk on vertex 𝑣") and having a fixed length 𝑛 as words over the set of vertices. Such a word corresponds to the sequence v=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)=v as defined in df-clwlks 30391. The set ((𝑣(ClWWalksNOn‘𝑔)𝑛) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.)
⊢ ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣}))
Theorem	clwwlknonmpo 30713*	(ClWWalksNOn‘𝐺) is an operator mapping a vertex 𝑣 and a nonnegative integer 𝑛 to the set of closed walks on 𝑣 of length 𝑛 as words over the set of vertices in a graph 𝐺. (Contributed by AV, 25-Feb-2022.) (Proof shortened by AV, 2-Mar-2024.)
⊢ (ClWWalksNOn‘𝐺) = (𝑣 ∈ (Vtx‘𝐺), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})
Theorem	clwwlknon 30714*	The set of closed walks on vertex 𝑋 of length 𝑁 in a graph 𝐺 as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
⊢ (𝑋(ClWWalksNOn‘𝐺)𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}
Theorem	isclwwlknon 30715	A word over the set of vertices representing a closed walk on vertex 𝑋 of length 𝑁 in a graph 𝐺. (Contributed by AV, 25-Feb-2022.) (Revised by AV, 24-Mar-2022.)
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋))
Theorem	clwwlk0on0 30716	There is no word over the set of vertices representing a closed walk on vertex 𝑋 of length 0 in a graph 𝐺. (Contributed by AV, 17-Feb-2022.) (Revised by AV, 25-Feb-2022.)
⊢ (𝑋(ClWWalksNOn‘𝐺)0) = ∅
Theorem	clwwlknon0 30717	Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022.)
⊢ (¬ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ) → (𝑋(ClWWalksNOn‘𝐺)𝑁) = ∅)
Theorem	clwwlknonfin 30718	In a finite graph 𝐺, the set of closed walks on vertex 𝑋 of length 𝑁 is also finite. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin)
Theorem	clwwlknonel 30719*	Characterization of a word over the set of vertices representing a closed walk on vertex 𝑋 of (nonzero) length 𝑁 in a graph 𝐺. This theorem would not hold for 𝑁 = 0 if 𝑊 = 𝑋 = ∅. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ≠ 0 → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = 𝑁 ∧ (𝑊‘0) = 𝑋)))
Theorem	clwwlknonccat 30720	The concatenation of two words representing closed walks on a vertex 𝑋 represents a closed walk on vertex 𝑋. The resulting walk is a "double loop", starting at vertex 𝑋, coming back to 𝑋 by the first walk, following the second walk and finally coming back to 𝑋 again. (Contributed by AV, 24-Apr-2022.)
⊢ ((𝐴 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑀) ∧ 𝐵 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) → (𝐴 ++ 𝐵) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑀 + 𝑁)))
Theorem	clwwlknon1 30721*	The set of closed walks on vertex 𝑋 of length 1 in a graph 𝐺 as words over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋𝐶1) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 = ⟨“𝑋”⟩ ∧ {𝑋} ∈ 𝐸)})
Theorem	clwwlknon1loop 30722	If there is a loop at vertex 𝑋, the set of (closed) walks on 𝑋 of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of 𝑋. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ {𝑋} ∈ 𝐸) → (𝑋𝐶1) = {⟨“𝑋”⟩})
Theorem	clwwlknon1nloop 30723	If there is no loop at vertex 𝑋, the set of (closed) walks on 𝑋 of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ({𝑋} ∉ 𝐸 → (𝑋𝐶1) = ∅)
Theorem	clwwlknon1sn 30724	The set of (closed) walks on vertex 𝑋 of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of 𝑋 iff there is a loop at 𝑋. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((𝑋𝐶1) = {⟨“𝑋”⟩} ↔ {𝑋} ∈ 𝐸))
Theorem	clwwlknon1le1 30725	There is at most one (closed) walk on vertex 𝑋 of length 1 as word over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.)
⊢ (♯‘(𝑋(ClWWalksNOn‘𝐺)1)) ≤ 1
Theorem	clwwlknon2 30726*	The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Revised by AV, 25-Mar-2022.)
⊢ 𝐶 = (ClWWalksNOn‘𝐺)    ⇒   ⊢ (𝑋𝐶2) = {𝑤 ∈ (2 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}
Theorem	clwwlknon2x 30727*	The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.)
⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋𝐶2) = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)}
Theorem	s2elclwwlknon2 30728	Sufficient conditions of a doubleton word to represent a closed walk on vertex 𝑋 of length 2. (Contributed by AV, 11-May-2022.)
⊢ 𝐶 = (ClWWalksNOn‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ {𝑋, 𝑌} ∈ 𝐸) → ⟨“𝑋𝑌”⟩ ∈ (𝑋𝐶2))
Theorem	clwwlknon2num 30729	In a 𝐾-regular graph 𝐺, there are 𝐾 closed walks on vertex 𝑋 of length 2. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.)
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾)
Theorem	clwwlknonwwlknonb 30730	A word over vertices represents a closed walk of a fixed length 𝑁 on vertex 𝑋 iff the word concatenated with 𝑋 represents a walk of length 𝑁 on 𝑋 and 𝑋. This theorem would not hold for 𝑁 = 0 and 𝑊 = ∅, see clwwlknwwlksnb 30679. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋)))
Theorem	clwwlknonex2lem1 30731	Lemma 1 for clwwlknonex2 30733: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for 𝑁 = 2, i.e., (♯‘𝑊) = 0, because (0..^(((♯‘𝑊) + 2) − 1)) = (0..^((0 + 2) − 1)) = (0..^1) = {0} ≠ { -1, 0} = (∅ ∪ { -1, 0}) = ((0..^(0 − 1)) ∪ {(0 − 1), 0}) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (0..^(((♯‘𝑊) + 2) − 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}))
Theorem	clwwlknonex2lem2 30732*	Lemma 2 for clwwlknonex2 30733: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑖), (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑖 + 1))} ∈ 𝐸)
Theorem	clwwlknonex2 30733	Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ (𝑁 ClWWalksN 𝐺))
Theorem	clwwlknonex2e 30734	Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk on vertex 𝑋. (Contributed by AV, 17-Apr-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁))
Theorem	clwwlknondisj 30735*	The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.)
⊢ Disj 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁)
Theorem	clwwlknun 30736*	The set of closed walks of fixed length 𝑁 in a simple graph 𝐺 is the union of the closed walks of the fixed length 𝑁 on each of the vertices of graph 𝐺. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (𝑁 ClWWalksN 𝐺) = ∪ 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁))
Theorem	clwwlkvbij 30737*	There is a bijection between the set of closed walks of a fixed length 𝑁 on a fixed vertex 𝑋 represented by walks (as word) and the set of closed walks (as words) of the fixed length 𝑁 on the fixed vertex 𝑋. The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 7-Jul-2022.) (Proof shortened by AV, 2-Nov-2022.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}⟶1-1onto(𝑋(ClWWalksNOn‘𝐺)𝑁))
17.3.11  Examples for walks, trails and paths
Theorem	0ewlk 30738	The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) → ∅ ∈ (𝐺 EdgWalks 𝑆))
Theorem	1ewlk 30739	A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.)
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom (iEdg‘𝐺)) → ⟨“𝐼”⟩ ∈ (𝐺 EdgWalks 𝑆))
Theorem	0wlk 30740	A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (∅(Walks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	is0wlk 30741	A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃 = {⟨0, 𝑁⟩} ∧ 𝑁 ∈ 𝑉) → ∅(Walks‘𝐺)𝑃)
Theorem	0wlkonlem1 30742	Lemma 1 for 0wlkon 30744 and 0trlon 30748. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	0wlkonlem2 30743	Lemma 2 for 0wlkon 30744 and 0trlon 30748. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0)))
Theorem	0wlkon 30744	A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(WalksOn‘𝐺)𝑁)𝑃)
Theorem	0wlkons1 30745	A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)⟨“𝑁”⟩)
Theorem	0trl 30746	A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑈 → (∅(Trails‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	is0trl 30747	A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃 = {⟨0, 𝑁⟩} ∧ 𝑁 ∈ 𝑉) → ∅(Trails‘𝐺)𝑃)
Theorem	0trlon 30748	A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(TrailsOn‘𝐺)𝑁)𝑃)
Theorem	0pth 30749	A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (∅(Paths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	0spth 30750	A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (∅(SPaths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	0pthon 30751	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃)
Theorem	0pthon1 30752	A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(PathsOn‘𝐺)𝑁){⟨0, 𝑁⟩})
Theorem	0pthonv 30753*	For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑁)𝑝)
Theorem	0clwlk 30754	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.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑋 → (∅(ClWalks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉))
Theorem	0clwlkv 30755	Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃:{0}⟶{𝑋}) → 𝐹(ClWalks‘𝐺)𝑃)
Theorem	0clwlk0 30756	There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
⊢ (ClWalks‘∅) = ∅
Theorem	0crct 30757	A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ (𝐺 ∈ 𝑊 → (∅(Circuits‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺)))
Theorem	0cycl 30758	A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.)
⊢ (𝐺 ∈ 𝑊 → (∅(Cycles‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺)))
Theorem	1pthdlem1 30759	Lemma 1 for 1pthd 30767. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹)))
Theorem	1pthdlem2 30760	Lemma 2 for 1pthd 30767. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅
Theorem	1wlkdlem1 30761	Lemma 1 for 1wlkd 30765. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	1wlkdlem2 30762	Lemma 2 for 1wlkd 30765. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽))
Theorem	1wlkdlem3 30763	Lemma 3 for 1wlkd 30765. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
Theorem	1wlkdlem4 30764*	Lemma 4 for 1wlkd 30765. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
Theorem	1wlkd 30765	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
Theorem	1trld 30766	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
Theorem	1pthd 30767	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
Theorem	1pthond 30768	In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃)
Theorem	upgr1wlkdlem1 30769	Lemma 1 for upgr1wlkd 30771. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → ((iEdg‘𝐺)‘𝐽) = {𝑋})
Theorem	upgr1wlkdlem2 30770	Lemma 2 for upgr1wlkd 30771. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ ((iEdg‘𝐺)‘𝐽))
Theorem	upgr1wlkd 30771	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
Theorem	upgr1trld 30772	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
Theorem	upgr1pthd 30773	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
Theorem	upgr1pthond 30774	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃)
Theorem	lppthon 30775	A loop (which is an edge at index 𝐽) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ⟨“𝐽”⟩(𝐴(PathsOn‘𝐺)𝐴)⟨“𝐴𝐴”⟩)
Theorem	lp1cycl 30776	A loop (which is an edge at index 𝐽) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ⟨“𝐽”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩)
Theorem	loop1cycl 30777*	A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)
⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))
Theorem	2cycld 30778	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	umgr2cycllem 30779*	Lemma for umgr2cycl 30780. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐽 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)
Theorem	umgr2cycl 30780*	A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ ∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))
17.3.12  Acyclic graphs
Syntax	cacycgr 30781	Extend class notation with acyclic graphs.
class AcyclicGraph
Definition	df-acycgr 30782*	Define the class of all acyclic graphs. A graph is called acyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
Theorem	dfacycgr1 30783*	An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
Theorem	isacycgr 30784*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)))
Theorem	isacycgr1 30785*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅)))
Theorem	acycgrcycl 30786	Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → 𝐹 = ∅)
Theorem	1pthon2v 30787*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝)
Theorem	1pthon2ve 30788*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Proof shortened by AV, 15-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ {𝐴, 𝐵} ∈ 𝐸) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝)
Theorem	wlk2v2elem1 30789	Lemma 1 for wlk2v2e 30791: 𝐹 is a length 2 word of over {0}, the domain of the singleton word 𝐼. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    ⇒   ⊢ 𝐹 ∈ Word dom 𝐼
Theorem	wlk2v2elem2 30790*	Lemma 2 for wlk2v2e 30791: The values of 𝐼 after 𝐹 are edges between two vertices enumerated by 𝑃. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    ⇒   ⊢ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}
Theorem	wlk2v2e 30791	In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    &   ⊢ 𝐺 = ⟨{𝑋, 𝑌}, 𝐼⟩    ⇒   ⊢ 𝐹(Walks‘𝐺)𝑃
Theorem	ntrl2v2e 30792	A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e 30791, but not a trail. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    &   ⊢ 𝐺 = ⟨{𝑋, 𝑌}, 𝐼⟩    ⇒   ⊢ ¬ 𝐹(Trails‘𝐺)𝑃
Theorem	3wlkdlem1 30793	Lemma 1 for 3wlkd 30804. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1)
Theorem	3wlkdlem2 30794	Lemma 2 for 3wlkd 30804. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (0..^(♯‘𝐹)) = {0, 1, 2}
Theorem	3wlkdlem3 30795	Lemma 3 for 3wlkd 30804. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)))
Theorem	3wlkdlem4 30796*	Lemma 4 for 3wlkd 30804. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)
Theorem	3wlkdlem5 30797*	Lemma 5 for 3wlkd 30804. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	3pthdlem1 30798*	Lemma 1 for 3pthd 30808. (Contributed by AV, 9-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗)))
Theorem	3wlkdlem6 30799	Lemma 6 for 3wlkd 30804. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾) ∧ 𝐶 ∈ (𝐼‘𝐿)))
Theorem	3wlkdlem7 30800	Lemma 7 for 3wlkd 30804. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V))