P. 297 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29601-29700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wlkp1lem3 29601	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
Theorem	wlkp1lem4 29602	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
Theorem	wlkp1lem5 29603*	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘))
Theorem	wlkp1lem6 29604*	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))))
Theorem	wlkp1lem7 29605	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))
Theorem	wlkp1lem8 29606*	Lemma for wlkp1 29607. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))
Theorem	wlkp1 29607	Append one path segment (edge) 𝐸 from vertex (𝑃‘𝑁) to a vertex 𝐶 to a walk ⟨𝐹, 𝑃⟩ to become a walk ⟨𝐻, 𝑄⟩ of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 30143. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 6-Mar-2021.) (Proof shortened by AV, 18-Apr-2021.) (Revised by AV, 8-Apr-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)
Theorem	wlkdlem1 29608*	Lemma 1 for wlkd 29612. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkdlem2 29609*	Lemma 2 for wlkd 29612. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (((♯‘𝐹) ∈ ℕ → (𝑃‘(♯‘𝐹)) ∈ (𝐼‘(𝐹‘((♯‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))))
Theorem	wlkdlem3 29610*	Lemma 3 for wlkd 29612. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
Theorem	wlkdlem4 29611*	Lemma 4 for wlkd 29612. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
Theorem	wlkd 29612*	Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
17.3.2  Walks for loop-free graphs
Theorem	lfgrwlkprop 29613*	Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	lfgriswlk 29614*	Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	lfgrwlknloop 29615*	In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
17.3.3  Trails
Syntax	ctrls 29616	Extend class notation with trails (within a graph).
class Trails
Syntax	ctrlson 29617	Extend class notation with trails between two vertices (within a graph).
class TrailsOn
Definition	df-trls 29618*	Define the set of all Trails (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ Trails = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ Fun ◡𝑓)})
Definition	df-trlson 29619*	Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Trails‘𝑔)𝑝)}))
Theorem	reltrls 29620	The set (Trails‘𝐺) of all trails on 𝐺 is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.)
⊢ Rel (Trails‘𝐺)
Theorem	trlsfval 29621*	The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
⊢ (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑓)}
Theorem	istrl 29622	Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))
Theorem	trliswlk 29623	A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	trlf1 29624	The enumeration 𝐹 of a trail ⟨𝐹, 𝑃⟩ is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼)
Theorem	trlreslem 29625	Lemma for trlres 29626. Formerly part of proof of eupthres 30142. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    ⇒   ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))–1-1-onto→dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
Theorem	trlres 29626	The restriction ⟨𝐻, 𝑄⟩ of a trail ⟨𝐹, 𝑃⟩ to an initial segment of the trail (of length 𝑁) forms a trail on the subgraph 𝑆 consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))    ⇒   ⊢ (𝜑 → 𝐻(Trails‘𝑆)𝑄)
Theorem	upgrtrls 29627*	The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (Trails‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ ((𝑓 ∈ Word dom 𝐼 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
Theorem	upgristrl 29628*	Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	upgrf1istrl 29629*	Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	wksonproplem 29630*	Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 29634. (Contributed by AV, 16-Jan-2021.) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))    &   ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)}))    ⇒   ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))
Theorem	wksonproplemOLD 29631*	Obsolete version of wksonproplem 29630 as of 13-Dec-2024. (Contributed by AV, 16-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))    &   ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)}))    &   ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑓(𝑄‘𝐺)𝑝) → 𝑓(Walks‘𝐺)𝑝)    ⇒   ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃)))
Theorem	trlsonfval 29632*	The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(TrailsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Trails‘𝐺)𝑝)})
Theorem	istrlson 29633	Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃)))
Theorem	trlsonprop 29634	Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃)))
Theorem	trlsonistrl 29635	A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.)
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	trlsonwlkon 29636	A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.)
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃)
Theorem	trlontrl 29637	A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹((𝑃‘0)(TrailsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
17.3.4  Paths and simple paths
Syntax	cpths 29638	Extend class notation with paths (of a graph).
class Paths
Syntax	cspths 29639	Extend class notation with simple paths (of a graph).
class SPaths
Syntax	cpthson 29640	Extend class notation with paths between two vertices (within a graph).
class PathsOn
Syntax	cspthson 29641	Extend class notation with simple paths between two vertices (within a graph).
class SPathsOn
Definition	df-pths 29642*	Define the set of all paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 29667). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ Paths = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)})
Definition	df-spths 29643*	Define the set of all simple paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ SPaths = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡𝑝)})
Definition	df-pthson 29644*	Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ PathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)}))
Definition	df-spthson 29645*	Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.)
⊢ SPathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPaths‘𝑔)𝑝)}))
Theorem	relpths 29646	The set (Paths‘𝐺) of all paths on 𝐺 is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.)
⊢ Rel (Paths‘𝐺)
Theorem	pthsfval 29647*	The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (Paths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)}
Theorem	spthsfval 29648*	The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡𝑝)}
Theorem	ispth 29649	Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
Theorem	isspth 29650	Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃))
Theorem	pthistrl 29651	A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	spthispth 29652	A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthiswlk 29653	A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	spthiswlk 29654	A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	pthdivtx 29655	The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(♯‘𝐹)) ∧ 𝐽 ∈ (0...(♯‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽))
Theorem	pthdadjvtx 29656	The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 𝐼 ∈ (0..^(♯‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1)))
Theorem	dfpth2 29657	Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
Theorem	pthdifv 29658	The vertices of a path are distinct (except the first and last vertex), so the restricted vertex function is one-to-one. (Contributed by AV, 2-Oct-2025.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	2pthnloop 29659*	A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 30078. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖))))
Theorem	upgr2pthnlp 29660*	A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))(♯‘(𝐼‘(𝐹‘𝑖))) = 2)
Theorem	spthdifv 29661	The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))–1-1→(Vtx‘𝐺))
Theorem	spthdep 29662	A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(SPaths‘𝐺)𝑃 ∧ (♯‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))
Theorem	pthdepisspth 29663	A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	upgrwlkdvdelem 29664*	Lemma for upgrwlkdvde 29665. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.)
⊢ ((𝑃:(0...(♯‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))
Theorem	upgrwlkdvde 29665	In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29666. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹)
Theorem	upgrspthswlk 29666*	The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝐺 ∈ UPGraph → (SPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)})
Theorem	upgrwlkdvspth 29667	A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29666. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	pthsonfval 29668*	The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(PathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Paths‘𝐺)𝑝)})
Theorem	spthson 29669*	The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(SPathsOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(SPaths‘𝐺)𝑝)})
Theorem	ispthson 29670	Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	isspthson 29671	Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthsonprop 29672	Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃)))
Theorem	spthonprop 29673	Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃)))
Theorem	pthonispth 29674	A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(Paths‘𝐺)𝑃)
Theorem	pthontrlon 29675	A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃)
Theorem	pthonpth 29676	A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
Theorem	isspthonpth 29677	A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)))
Theorem	spthonisspth 29678	A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(SPaths‘𝐺)𝑃)
Theorem	spthonpthon 29679	A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃)
Theorem	spthonepeq 29680	The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (♯‘𝐹) = 0))
Theorem	uhgrwkspthlem1 29681	Lemma 1 for uhgrwkspth 29683. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹)
Theorem	uhgrwkspthlem2 29682	Lemma 2 for uhgrwkspth 29683. (Contributed by AV, 25-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃)
Theorem	uhgrwkspth 29683	Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.)
⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2wlkneq 29684	The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1)))
Theorem	usgr2wlkspthlem1 29685	Lemma 1 for usgr2wlkspth 29687. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹)
Theorem	usgr2wlkspthlem2 29686	Lemma 2 for usgr2wlkspth 29687. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃)
Theorem	usgr2wlkspth 29687	In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃))
Theorem	usgr2trlncl 29688	In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2)))
Theorem	usgr2trlspth 29689	In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthspth 29690	In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Paths‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃))
Theorem	usgr2pthlem 29691*	Lemma for usgr2pth 29692. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))
Theorem	usgr2pth 29692*	In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))))
Theorem	usgr2pth0 29693*	In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦})))))
Theorem	pthdlem1 29694*	Lemma 1 for pthd 29697. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅)))
Theorem	pthdlem2lem 29695*	Lemma for pthdlem2 29696. (Contributed by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅)))
Theorem	pthdlem2 29696*	Lemma 2 for pthd 29697. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    ⇒   ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)
Theorem	pthd 29697*	Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ 𝑅 = ((♯‘𝑃) − 1)    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗)))    &   ⊢ (♯‘𝐹) = 𝑅    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
17.3.5  Closed walks
Syntax	cclwlks 29698	Extend class notation with closed walks (of a graph).
class ClWalks
Definition	df-clwlks 29699*	Define the set of all closed walks (in an undirected graph). According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex can be considered as a closed walk of length 0, see also 0clwlk 30057. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.)
⊢ ClWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))})
Theorem	clwlks 29700*	The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Revised by AV, 29-Oct-2021.)
⊢ (ClWalks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}