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	erclwwlkn 30001*	∼ 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 30002*	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 30003*	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 30004*	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 30005*	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 30006*	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 30007*	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 30008*	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 30009	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 30010	Lemma 1 for clwlknf1oclwwlkn 30013. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝐶))) → (♯‘((2nd ‘𝐶) prefix ((♯‘(2nd ‘𝐶)) − 1))) = (♯‘(1st ‘𝐶)))
Theorem	clwlknf1oclwwlknlem2 30011*	Lemma 2 for clwlknf1oclwwlkn 30013: 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 30012*	Lemma 3 for clwlknf1oclwwlkn 30013: The bijective function of clwlknf1oclwwlkn 30013 is the bijective function of clwlkclwwlkf1o 29940 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 30013*	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 30014*	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 30015*	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 30016	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 30017*	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 29701. 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 30018*	(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 30019*	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 30020	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 30021	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 30022	Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022.)
⊢ (¬ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ) → (𝑋(ClWWalksNOn‘𝐺)𝑁) = ∅)
Theorem	clwwlknonfin 30023	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 30024*	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 30025	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 30026*	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 30027	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 30028	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 30029	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 30030	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 30031*	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 30032*	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 30033	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 30034	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 30035	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 29984. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ ⟨“𝑋”⟩) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋)))
Theorem	clwwlknonex2lem1 30036	Lemma 1 for clwwlknonex2 30038: 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 30037*	Lemma 2 for clwwlknonex2 30038: 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 30038	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 30039	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 30040*	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 30041*	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 30042*	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 30043	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 30044	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 30045	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 30046	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 30047	Lemma 1 for 0wlkon 30049 and 0trlon 30053. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
Theorem	0wlkonlem2 30048	Lemma 2 for 0wlkon 30049 and 0trlon 30053. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0)))
Theorem	0wlkon 30049	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 30050	A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)⟨“𝑁”⟩)
Theorem	0trl 30051	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 30052	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 30053	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 30054	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 30055	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 30056	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 30057	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 30058*	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 30059	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 30060	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 30061	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 30062	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 30063	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 30064	Lemma 1 for 1pthd 30072. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹)))
Theorem	1pthdlem2 30065	Lemma 2 for 1pthd 30072. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    ⇒   ⊢ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅
Theorem	1wlkdlem1 30066	Lemma 1 for 1wlkd 30070. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	1wlkdlem2 30067	Lemma 2 for 1wlkd 30070. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽))
Theorem	1wlkdlem3 30068	Lemma 3 for 1wlkd 30070. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
Theorem	1wlkdlem4 30069*	Lemma 4 for 1wlkd 30070. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋})    &   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
Theorem	1wlkd 30070	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 30071	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 30072	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 30073	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 30074	Lemma 1 for upgr1wlkd 30076. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → ((iEdg‘𝐺)‘𝐽) = {𝑋})
Theorem	upgr1wlkdlem2 30075	Lemma 2 for upgr1wlkd 30076. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ ((iEdg‘𝐺)‘𝐽))
Theorem	upgr1wlkd 30076	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 30077	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 30078	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 30079	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 30080	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 30081	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 30082*	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 30083*	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 30084	Lemma 1 for wlk2v2e 30086: 𝐹 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 30085*	Lemma 2 for wlk2v2e 30086: 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 30086	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 30087	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 30086, 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 30088	Lemma 1 for 3wlkd 30099. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1)
Theorem	3wlkdlem2 30089	Lemma 2 for 3wlkd 30099. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (0..^(♯‘𝐹)) = {0, 1, 2}
Theorem	3wlkdlem3 30090	Lemma 3 for 3wlkd 30099. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)))
Theorem	3wlkdlem4 30091*	Lemma 4 for 3wlkd 30099. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)
Theorem	3wlkdlem5 30092*	Lemma 5 for 3wlkd 30099. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	3pthdlem1 30093*	Lemma 1 for 3pthd 30103. (Contributed by AV, 9-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗)))
Theorem	3wlkdlem6 30094	Lemma 6 for 3wlkd 30099. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾) ∧ 𝐶 ∈ (𝐼‘𝐿)))
Theorem	3wlkdlem7 30095	Lemma 7 for 3wlkd 30099. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V))
Theorem	3wlkdlem8 30096	Lemma 8 for 3wlkd 30099. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿))
Theorem	3wlkdlem9 30097	Lemma 9 for 3wlkd 30099. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))
Theorem	3wlkdlem10 30098*	Lemma 10 for 3wlkd 30099. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))
Theorem	3wlkd 30099	Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 24-Mar-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
Theorem	3wlkond 30100	A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐷)𝑃)