P. 300 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29901-30000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgrwlkcompim 29901*	Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 14-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (Walks‘𝐺)) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))
Theorem	wlkvtxedg 29902*	The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ 𝐸 {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒)
Theorem	upgrwlkvtxedg 29903*	The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
Theorem	uspgr2wlkeq 29904*	Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.)
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ 𝑁 = (♯‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦))))
Theorem	uspgr2wlkeq2 29905	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.)
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘𝐵)) = 𝑁)) → ((2nd ‘𝐴) = (2nd ‘𝐵) → 𝐴 = 𝐵))
Theorem	uspgr2wlkeqi 29906	Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021.)
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) → 𝐴 = 𝐵)
Theorem	umgrwlknloop 29907*	In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	wlkv0 29908	If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
⊢ (((Vtx‘𝐺) = ∅ ∧ 𝑊 ∈ (Walks‘𝐺)) → ((1st ‘𝑊) = ∅ ∧ (2nd ‘𝑊) = ∅))
Theorem	g0wlk0 29909	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
⊢ ((Vtx‘𝐺) = ∅ → (Walks‘𝐺) = ∅)
Theorem	0wlk0 29910	There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
⊢ (Walks‘∅) = ∅
Theorem	wlk0prc 29911	There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.)
⊢ ((𝑆 ∉ V ∧ (Vtx‘𝑆) = (Vtx‘𝐺)) → (Walks‘𝐺) = ∅)
Theorem	wlklenvclwlk 29912	The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by JJ, 14-Jan-2024.)
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (⟨𝐹, (𝑊 ++ ⟨“(𝑊‘0)”⟩)⟩ ∈ (Walks‘𝐺) → (♯‘𝐹) = (♯‘𝑊)))
Theorem	wlkson 29913*	The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 30-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(WalksOn‘𝐺)𝐵) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(♯‘𝑓)) = 𝐵)})
Theorem	iswlkon 29914	Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 31-Dec-2020.) (Revised by AV, 22-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)))
Theorem	wlkonprop 29915	Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 31-Dec-2020.) (Proof shortened by AV, 16-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)))
Theorem	wlkpvtx 29916	A walk connects vertices. (Contributed by AV, 22-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑁 ∈ (0...(♯‘𝐹)) → (𝑃‘𝑁) ∈ 𝑉))
Theorem	wlkepvtx 29917	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘(♯‘𝐹)) ∈ 𝑉))
Theorem	wlkoniswlk 29918	A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 2-Jan-2021.)
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	wlkonwlk 29919	A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹((𝑃‘0)(WalksOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃)
Theorem	wlkonwlk1l 29920	A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 22-Mar-2021.)
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → 𝐹((𝑃‘0)(WalksOn‘𝐺)(lastS‘𝑃))𝑃)
Theorem	wlksoneq1eq2 29921	Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.)
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	wlkonl1iedg 29922*	If there is a walk between two vertices 𝐴 and 𝐵 at least of length 1, then the start vertex 𝐴 is incident with an edge. (Contributed by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (♯‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒)
Theorem	wlkon2n0 29923	The length of a walk between two different vertices is not 0 (i.e. is at least 1). (Contributed by AV, 3-Apr-2021.)
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐴 ≠ 𝐵) → (♯‘𝐹) ≠ 0)
Theorem	2wlklem 29924*	Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
⊢ (∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
Theorem	upgr2wlk 29925	Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 28-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))))
Theorem	wlkreslem 29926	Lemma for wlkres 29927. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → 𝑆 ∈ V)
Theorem	wlkres 29927	The restriction ⟨𝐻, 𝑄⟩ of a walk ⟨𝐹, 𝑃⟩ to an initial segment of the walk (of length 𝑁) forms a walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 30475. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    &   ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))    ⇒   ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)
Theorem	redwlklem 29928	Lemma for redwlk 29929. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(♯‘𝐹))):(0...(♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))))⟶𝑉)
Theorem	redwlk 29929	A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (♯‘𝐹)) → (𝐹 ↾ (0..^((♯‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(♯‘𝐹))))
Theorem	wlkp1lem1 29930	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    ⇒   ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃)
Theorem	wlkp1lem2 29931	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1))
Theorem	wlkp1lem3 29932	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
Theorem	wlkp1lem4 29933	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
Theorem	wlkp1lem5 29934*	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘))
Theorem	wlkp1lem6 29935*	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))))
Theorem	wlkp1lem7 29936	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))
Theorem	wlkp1lem8 29937*	Lemma for wlkp1 29938. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))
Theorem	wlkp1 29938	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 30476. (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 29939*	Lemma 1 for wlkd 29943. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkdlem2 29940*	Lemma 2 for wlkd 29943. (Contributed by AV, 7-Feb-2021.)
⊢ (𝜑 → 𝑃 ∈ Word V)    &   ⊢ (𝜑 → 𝐹 ∈ Word V)    &   ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (((♯‘𝐹) ∈ ℕ → (𝑃‘(♯‘𝐹)) ∈ (𝐼‘(𝐹‘((♯‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))))
Theorem	wlkdlem3 29941*	Lemma 3 for wlkd 29943. (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 29942*	Lemma 4 for wlkd 29943. (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 29943*	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 29944*	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 29945*	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 29946*	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 29947	Extend class notation with trails (within a graph).
class Trails
Syntax	ctrlson 29948	Extend class notation with trails between two vertices (within a graph).
class TrailsOn
Definition	df-trls 29949*	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 29950*	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 29951	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 29952*	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 29953	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 29954	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 29955	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 29956	Lemma for trlres 29957. Formerly part of proof of eupthres 30475. (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 29957	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 29958*	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 29959*	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 29960*	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 29961*	Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 29964. (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	trlsonfval 29962*	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 29963	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 29964	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 29965	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 29966	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 29967	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 29968	Extend class notation with paths (of a graph).
class Paths
Syntax	cspths 29969	Extend class notation with simple paths (of a graph).
class SPaths
Syntax	cpthson 29970	Extend class notation with paths between two vertices (within a graph).
class PathsOn
Syntax	cspthson 29971	Extend class notation with simple paths between two vertices (within a graph).
class SPathsOn
Definition	df-pths 29972*	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 29997). 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 29973*	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 29974*	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 29975*	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 29976	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 29977*	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 29978*	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 29979	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 29980	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 29981	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 29982	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 29983	A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.)
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	spthiswlk 29984	A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.)
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	pthdivtx 29985	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 29986	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 29987	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 29988	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 29989*	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 30411. (Contributed by AV, 6-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖))))
Theorem	upgr2pthnlp 29990*	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 29991	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 29992	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 29993	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 29994*	Lemma for upgrwlkdvde 29995. (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 29995	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 29996. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹)
Theorem	upgrspthswlk 29996*	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 29997	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 29996. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	pthsonfval 29998*	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 29999*	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 30000	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‘𝐺)𝑃)))