P. 301 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30001-30100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	umgr2cwwkdifex 30001*	If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ (ℤ≥‘2) ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺)) → ∃𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) ≠ (𝑊‘0))
Theorem	erclwwlknrel 30002	∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ Rel ∼
Theorem	erclwwlkneq 30003*	Two classes are equivalent regarding ∼ if both are words of the same fixed length and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 ↔ (𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛))))
Theorem	erclwwlkneqlen 30004*	If two classes are equivalent regarding ∼, then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 → (♯‘𝑇) = (♯‘𝑈)))
Theorem	erclwwlknref 30005*	∼ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018.) (Revised by AV, 30-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥)
Theorem	erclwwlknsym 30006*	∼ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥)
Theorem	erclwwlkntr 30007*	∼ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)
Theorem	erclwwlkn 30008*	∼ is an equivalence relation over the set of closed walks (defined as words) with a fixed length. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ∼ Er 𝑊
Theorem	qerclwwlknfi 30009*	The quotient set of the set of closed walks (defined as words) with a fixed length according to the equivalence relation ∼ is finite. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑊 / ∼ ) ∈ Fin)
Theorem	hashclwwlkn0 30010*	The number of closed walks (defined as words) with a fixed length is the sum of the sizes of all equivalence classes according to ∼. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘𝑊) = Σ𝑥 ∈ (𝑊 / ∼ )(♯‘𝑥))
Theorem	eclclwwlkn1 30011*	An equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)}))
Theorem	eleclclwwlkn 30012*	A member of an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 1-May-2021.)
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺)    &   ⊢ ∼ = {⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))}    ⇒   ⊢ ((𝐵 ∈ (𝑊 / ∼ ) ∧ 𝑋 ∈ 𝐵) → (𝑌 ∈ 𝐵 ↔ (𝑌 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))))
Theorem	hashecclwwlkn1 30013*	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 30014*	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 30015*	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 30016	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 30017	Lemma 1 for clwlknf1oclwwlkn 30020. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝐶))) → (♯‘((2nd ‘𝐶) prefix ((♯‘(2nd ‘𝐶)) − 1))) = (♯‘(1st ‘𝐶)))
Theorem	clwlknf1oclwwlknlem2 30018*	Lemma 2 for clwlknf1oclwwlkn 30020: 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 30019*	Lemma 3 for clwlknf1oclwwlkn 30020: The bijective function of clwlknf1oclwwlkn 30020 is the bijective function of clwlkclwwlkf1o 29947 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 30020*	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-1-onto→(𝑁 ClWWalksN 𝐺))
Theorem	clwlkssizeeq 30021*	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 30022*	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 30023	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 30024*	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 29708. 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 30025*	(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 30026*	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 30027	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 30028	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 30029	Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022.)
⊢ (¬ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ) → (𝑋(ClWWalksNOn‘𝐺)𝑁) = ∅)
Theorem	clwwlknonfin 30030	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 30031*	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 30032	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 30033*	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 30034	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 30035	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 30036	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 30037	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 30038*	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 30039*	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 30040	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 30041	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 30042	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 29991. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋)))
Theorem	clwwlknonex2lem1 30043	Lemma 1 for clwwlknonex2 30045: 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 30044*	Lemma 2 for clwwlknonex2 30045: 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 30045	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 30046	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 30047*	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 30048*	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 30049*	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-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁))
17.3.11  Examples for walks, trails and paths
Theorem	0ewlk 30050	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 30051	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 30052	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 30053	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 30054	Lemma 1 for 0wlkon 30056 and 0trlon 30060. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	0wlkonlem2 30055	Lemma 2 for 0wlkon 30056 and 0trlon 30060. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0)))
Theorem	0wlkon 30056	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 30057	A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)⟨“𝑁”⟩)
Theorem	0trl 30058	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 30059	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 30060	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 30061	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 30062	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 30063	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 30064	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 30065*	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 30066	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 30067	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 30068	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 30069	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 30070	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 30071	Lemma 1 for 1pthd 30079. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹)))
Theorem	1pthdlem2 30072	Lemma 2 for 1pthd 30079. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅
Theorem	1wlkdlem1 30073	Lemma 1 for 1wlkd 30077. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	1wlkdlem2 30074	Lemma 2 for 1wlkd 30077. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽))
Theorem	1wlkdlem3 30075	Lemma 3 for 1wlkd 30077. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
Theorem	1wlkdlem4 30076*	Lemma 4 for 1wlkd 30077. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
Theorem	1wlkd 30077	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 30078	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 30079	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 30080	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 30081	Lemma 1 for upgr1wlkd 30083. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → ((iEdg‘𝐺)‘𝐽) = {𝑋})
Theorem	upgr1wlkdlem2 30082	Lemma 2 for upgr1wlkd 30083. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ ((iEdg‘𝐺)‘𝐽))
Theorem	upgr1wlkd 30083	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 30084	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 30085	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 30086	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 30087	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 30088	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	1pthon2v 30089*	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 30090*	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 30091	Lemma 1 for wlk2v2e 30093: 𝐹 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 30092*	Lemma 2 for wlk2v2e 30093: 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 30093	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 30094	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 30093, 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 30095	Lemma 1 for 3wlkd 30106. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1)
Theorem	3wlkdlem2 30096	Lemma 2 for 3wlkd 30106. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (0..^(♯‘𝐹)) = {0, 1, 2}
Theorem	3wlkdlem3 30097	Lemma 3 for 3wlkd 30106. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)))
Theorem	3wlkdlem4 30098*	Lemma 4 for 3wlkd 30106. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)
Theorem	3wlkdlem5 30099*	Lemma 5 for 3wlkd 30106. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	3pthdlem1 30100*	Lemma 1 for 3pthd 30110. (Contributed by AV, 9-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗)))