P. 292 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29101-29200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0grrgr 29101	The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.)
⊢ ∀𝑘 ∈ ℕ0* ∅ RegGraph 𝑘
Theorem	cusgrrusgr 29102	A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 RegUSGraph ((♯‘𝑉) − 1))
Theorem	cusgrm1rusgr 29103	A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for 𝑘 ∈ ℤ, then the assumption 𝑉 ≠ ∅ could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ((♯‘𝑉) − 1)))
Theorem	rusgrpropnb 29104*	The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘(𝐺 NeighbVtx 𝑣)) = 𝐾))
Theorem	rusgrpropedg 29105*	The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020.) (Revised by AV, 27-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑒 ∈ (Edg‘𝐺) ∣ 𝑣 ∈ 𝑒}) = 𝐾))
Theorem	rusgrpropadjvtx 29106*	The properties of a k-regular simple graph expressed with adjacent vertices. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 27-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑘 ∈ 𝑉 ∣ {𝑣, 𝑘} ∈ (Edg‘𝐺)}) = 𝐾))
Theorem	rusgrnumwrdl2 29107*	In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 6-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾)
Theorem	rusgr1vtxlem 29108*	Lemma for rusgr1vtx 29109. (Contributed by AV, 27-Dec-2020.)
⊢ (((∀𝑣 ∈ 𝑉 (♯‘𝐴) = 𝐾 ∧ ∀𝑣 ∈ 𝑉 𝐴 = ∅) ∧ (𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 1)) → 𝐾 = 0)
Theorem	rusgr1vtx 29109	If a k-regular simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 27-Dec-2020.)
⊢ (((♯‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0)
Theorem	rgrusgrprc 29110*	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∈ USGraph ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rusgrprc 29111	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegUSGraph 0} ∉ V
Theorem	rgrprc 29112	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegGraph 0} ∉ V
Theorem	rgrprcx 29113*	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rgrx0ndm 29114*	0 is not in the domain of the potentially alternative definition of the sets of k-regular graphs for each extended nonnegative integer k. (Contributed by AV, 28-Dec-2020.)
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘})    ⇒   ⊢ 0 ∉ dom 𝑅
Theorem	rgrx0nd 29115*	The potentially alternatively defined k-regular graphs is not defined for k=0. (Contributed by AV, 28-Dec-2020.)
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘})    ⇒   ⊢ (𝑅‘0) = ∅
17.3  Walks, paths and cycles A "walk" in a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see definition of [Bollobas] p. 4, or "A walk (of length k) in a graph is a nonempty alternating sequence v0 e0 v1 e1 ... e(k-1) vk of vertices and edges in G such that ei = { vi , vi+1 } for all i < k.", see definition of [Diestel] p. 10. Formalizing these definitions (mainly by representing the indexed vertices and edges by functions), a walk is represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges (e is a third function enumerating the edges within the graph, not within the walk), and p enumerates the vertices, see df-wlks 29120. Hence a walk (of length n) is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Alternatively, one could define a walk as a function 𝑤:(0...(2 · 𝑛))⟶((Edg‘𝐺) ∪ (Vtx‘𝐺)) such that for all 0 ≤ 𝑘 ≤ 𝑛, (𝑤‘(2 · 𝑘)) ∈ (Vtx‘𝐺) and for all 0 ≤ 𝑘 ≤ (𝑛 − 1), (𝑤‘((2 · 𝑘) + 1)) ∈ (Edg‘𝐺) and {(𝑤‘(2 · 𝑘)), (𝑤‘((2 · 𝑘) + 2))} ⊆ (𝑤‘((2 · 𝑘) + 1)). Based on our definition of Walks, the class of all walks, more restrictive constructs are defined: * Trails (df-trls 29213): A "walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5, i.e., f(i) =/= f(j) if i =/= j. * Paths (df-pths 29237): A path is a walk whose vertices except the first and the last vertex are distinct, i.e., p(i) =/= p(j) if i < j, except possibly when i = 0 and j = n. * SPaths (simple paths, df-spths 29238): A simple path "is a walk with distinct vertices.", see Notation of [Bollobas] p. 5, i.e., p(i) =/= p(j) if i =/= j. * ClWalks (closed walks, df-clwlks 29292): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n). * Circuits (df-crcts 29307): "A trail whose endvertices coincide (a closed trail) is called a circuit." (see Definition of [Bollobas] p. 5), i.e., f(i) =/= f(j) if i =/= j and p(0) = p(n). Equivalently, a circuit is a closed walk with distinct edges. * Cycles (df-cycls 29308): A path whose endvertices coincide (a closed path) is called a cycle, i.e., p(i) =/= p(j) if i =/= j, except i = 0 and j = n, and p(0) = p(n). Equivalently, a cycle is a closed walk with distinct vertices. * EulerPaths (Eulerian paths, df-eupth 29715): An Eulerian path is "a trail containing all edges [of the graph]" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Note, however, that an Eulerian path needs not be a path. * Eulerian circuit: An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j, p(0) = p(n) and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Hierarchy of all kinds of walks (apply ssriv 3987 and elopabran 5563 to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk 29295, see clwlkwlk 29296 and clwlkswks 29297): * Trails are walks (trliswlk 29218): (Trails‘𝐺) ⊆ (Walks‘𝐺) * Paths are trails (pthistrl 29246): (Paths‘𝐺) ⊆ (Trails‘𝐺) * Simple paths are paths (spthispth 29247): (SPaths‘𝐺) ⊆ (Paths‘𝐺) * Closed walks are walks (clwlkiswlk 29295): (ClWalks‘𝐺) ⊆ (Walks‘𝐺) * Circuits are closed walks (crctisclwlk 29315): (Circuits‘𝐺) ⊆ (ClWalks‘𝐺) * Circuits are trails (crctistrl 29316): (Circuits‘𝐺) ⊆ (Trails‘𝐺) * Cycles are paths (cyclispth 29318): (Cycles‘𝐺) ⊆ (Paths‘𝐺) * Cycles are circuits (cycliscrct 29320): (Cycles‘𝐺) ⊆ (Circuits‘𝐺) * (Non-trivial) cycles are not simple paths (cyclnspth 29321): (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃)) * Eulerian paths are trails (eupthistrl 29728): (EulerPaths‘𝐺) ⊆ (Trails‘𝐺) Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e., omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14470, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definition df-wwlks 29348 for WWalks, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In this case, the general definitions of walks and the definition of walks as words are equivalent, see wlkiswwlks 29394. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). Based on this definition of WWalks, the class of all walks as word, more restrictive constructs are defined analogously to the general definition of a walk: * WWalksN (walks of length N as word, df-wwlksn 29349): n = N * WSPathsN (simple paths of length N as word, df-wspthsn 29351): p(i) =/= p(j) if i =/= j and n = N * ClWWalks (closed walks as word, df-clwwlk 29499): p(0) = p(n) * ClWWalksN (closed walks of length N as word, df-clwwlkn 29542): p(0) = p(n) and n = N Finally, there are a couple of definitions for (special) walks ⟨𝐹, 𝑃⟩ having fixed endpoints 𝐴 and 𝐵: * Walks with particular endpoints (df-wlkson 29121): 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 * Trails with particular endpoints (df-trlson 29214): 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 * Paths with particular endpoints (df-pthson 29239): 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 * Simple paths with particular endpoints (df-spthson 29240): 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 * Walks of a fixed length 𝑁 as words with particular endpoints (df-wwlksnon 29350): (𝐴(𝑁 WWalksNOn 𝐺)𝐵) * Simple paths of a fixed length 𝑁 as words with particular endpoints (df-wspthsnon 29352): (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) * Closed Walks of a fixed length 𝑁 as words anchored at a particular vertex 𝐴 (df-wwlksnon 29350): (𝐴(ClWWalksNOn‘𝐺)𝑁)
17.3.1  Walks A "walk" within a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. This definition requires the edges to connect two vertices at most (loops are also allowed: if e(i) is a loop, then x(i-1) = x(i)). For hypergraphs containing hyperedges (i.e. edges connecting more than two vertices), however, a more general definition is needed. Two approaches for a definition applicable for arbitrary hypergraphs are used in the literature: "walks on the vertex level" and "walks on the edge level" (see Aksoy, Joslyn, Marrero, Praggastis, Purvine: "Hypernetwork science via high-order hypergraph walks", June 2020, https://doi.org/10.1140/epjds/s13688-020-00231-0): "walks on the edge level": For a positive integer s, an s-walk of length k between hyperedges f and g is a sequence of hyperedges, f=e(0), e(1), ... , e(k)=g, where for j=1, ... , k, e(j-1) =/= e(j) and e(j-1) and e(j) have at least s vertices in common (according to Aksoy et al.). "walks on the vertex level": For a positive integer s, an s-walk of length k between vertices a and b is a sequence of vertices, a=v(0), v(1), ... , v(k)=b, where for j=1, ... , k, v(j-1) and v(j) are connected by at least s edges (analogous to Aksoy et al.). There are two imperfections for the definition for "walks on the edge level": one is that a walk of length 1 consists of two edges (or a walk of length 0 consists of one edge), whereas a walk of length 1 on the vertex level consists of two vertices and one edge (or a walk of length 0 consists of one vertex and no edge). The other is that edges, especially loops, can be traversed only once (and not repeatedly) because of the condition e(j-1) =/= e(j). The latter is avoided in the definition for EdgWalks, see df-ewlks 29119. To be compatible with the (usual) definition of walks for pseudographs, walks also suitable for arbitrary hypergraphs are defined "on the vertex level" in the following as Walks, see df-wlks 29120, restricting s to 1. wlk1ewlk 29161 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level".
Syntax	cewlks 29116	Extend class notation with s-walks "on the edge level" (of a hypergraph).
class EdgWalks
Syntax	cwlks 29117	Extend class notation with walks (i.e. 1-walks) (of a hypergraph).
class Walks
Syntax	cwlkson 29118	Extend class notation with walks between two vertices (within a graph).
class WalksOn
Definition	df-ewlks 29119*	Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., 𝑠 = 0 (a 0-walk is an arbitrary sequence of hyperedges) and 𝑠 = +∞ (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.)
⊢ EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})
Definition	df-wlks 29120*	Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" (see wlk1walk 29160) discussed in Aksoy et al. The predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk in a graph 𝐺", see also iswlk 29131. The condition {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) should be allowed only if there is a loop at (𝑝‘𝑘). Otherwise, C would be fulfilled by each edge containing (𝑝‘𝑘). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is 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 AV, 30-Dec-2020.)
⊢ Walks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))})
Definition	df-wlkson 29121*	Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkon 29178. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}))
Theorem	ewlksfval 29122*	The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*) → (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))})
Theorem	isewlk 29123*	Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈) → (𝐹 ∈ (𝐺 EdgWalks 𝑆) ↔ (𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))))
Theorem	ewlkprop 29124*	Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))
Theorem	ewlkinedg 29125	The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝐾 ∈ (1..^(♯‘𝐹))) → 𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝐾 − 1))) ∩ (𝐼‘(𝐹‘𝐾)))))
Theorem	ewlkle 29126	An s-walk of edges is also a t-walk of edges if 𝑡 ≤ 𝑠. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇))
Theorem	upgrewlkle2 29127	In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (♯‘𝐹)) → 𝑆 ≤ 2)
Theorem	wkslem1 29128	Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵)))))
Theorem	wkslem2 29129	Lemma 2 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)
⊢ ((𝐴 = 𝐵 ∧ (𝐴 + 1) = 𝐶) → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘𝐶), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘𝐶)} ⊆ (𝐼‘(𝐹‘𝐵)))))
Theorem	wksfval 29130*	The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (Walks‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))})
Theorem	iswlk 29131*	Properties of a pair of functions to be a walk. (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkprop 29132*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkv 29133	The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
Theorem	iswlkg 29134*	Generalization of iswlk 29131: Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑊 → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkf 29135	The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
Theorem	wlkcl 29136	A walk has length ♯(𝐹), which is an integer. Formerly proven for an Eulerian path, see eupthcl 29727. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0)
Theorem	wlkp 29137	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkpwrd 29138	The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ Word 𝑉)
Theorem	wlklenvp1 29139	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝑃) = ((♯‘𝐹) + 1))
Theorem	wksv 29140*	The class of walks is a set. (Contributed by AV, 15-Jan-2021.) (Proof shortened by SN, 11-Dec-2024.)
⊢ {⟨𝑓, 𝑝⟩ ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V
Theorem	wksvOLD 29141*	Obsolete version of wksv 29140 as of 11-Dec-2024. (Contributed by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {⟨𝑓, 𝑝⟩ ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V
Theorem	wlkn0 29142	The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ≠ ∅)
Theorem	wlklenvm1 29143	The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) = ((♯‘𝑃) − 1))
Theorem	ifpsnprss 29144	Lemma for wlkvtxeledg 29145: Two adjacent (not necessarily different) vertices 𝐴 and 𝐵 in a walk are incident with an edge 𝐸. (Contributed by AV, 4-Apr-2021.) (Revised by AV, 5-Nov-2021.)
⊢ (if-(𝐴 = 𝐵, 𝐸 = {𝐴}, {𝐴, 𝐵} ⊆ 𝐸) → {𝐴, 𝐵} ⊆ 𝐸)
Theorem	wlkvtxeledg 29145*	Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))
Theorem	wlkvtxiedg 29146*	The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒)
Theorem	relwlk 29147	The set (Walks‘𝐺) of all walks on 𝐺 is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 19-Feb-2021.)
⊢ Rel (Walks‘𝐺)
Theorem	wlkvv 29148	If there is at least one walk in the graph, all walks are in the universal class of ordered pairs. (Contributed by AV, 2-Jan-2021.)
⊢ ((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → 𝑊 ∈ (V × V))
Theorem	wlkop 29149	A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.)
⊢ (𝑊 ∈ (Walks‘𝐺) → 𝑊 = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩)
Theorem	wlkcpr 29150	A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.)
⊢ (𝑊 ∈ (Walks‘𝐺) ↔ (1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊))
Theorem	wlk2f 29151*	If there is a walk 𝑊 there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.)
⊢ (𝑊 ∈ (Walks‘𝐺) → ∃𝑓∃𝑝 𝑓(Walks‘𝐺)𝑝)
Theorem	wlkcomp 29152*	A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ ((𝐺 ∈ 𝑈 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (Walks‘𝐺) ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkcompim 29153*	Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkelwrd 29154	The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐹 = (1st ‘𝑊)    &   ⊢ 𝑃 = (2nd ‘𝑊)    ⇒   ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉))
Theorem	wlkeq 29155*	Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.)
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥))))
Theorem	edginwlk 29156	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ (0..^(♯‘𝐹))) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)
Theorem	upgredginwlk 29157	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼) → (𝐾 ∈ (0..^(♯‘𝐹)) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸))
Theorem	iedginwlk 29158	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((Fun 𝐼 ∧ 𝐹(Walks‘𝐺)𝑃 ∧ 𝑋 ∈ (0..^(♯‘𝐹))) → (𝐼‘(𝐹‘𝑋)) ∈ ran 𝐼)
Theorem	wlkl1loop 29159	A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021.)
⊢ (((Fun (iEdg‘𝐺) ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺))
Theorem	wlk1walk 29160*	A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (1..^(♯‘𝐹))1 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlk1ewlk 29161	A walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ (𝐺 EdgWalks 1))
Theorem	upgriswlk 29162*	Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 28-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	upgrwlkedg 29163*	The edges of a walk in a pseudograph join exactly the two corresponding adjacent vertices in the walk. (Contributed by AV, 27-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
Theorem	upgrwlkcompim 29164*	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 29165*	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 29166*	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 29167*	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 29168	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 29169	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 29170*	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	wlkResOLD 29171*	Obsolete version of opabresex2 7464 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 30-Dec-2020.) (Proof shortened by AV, 15-Jan-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑓(𝑊‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝)    ⇒   ⊢ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑊‘𝐺)𝑝 ∧ 𝜑)} ∈ V
Theorem	wlkv0 29172	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 29173	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 29174	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 29175	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 29176	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 29177*	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 29178	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 29179	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 29180	A walk connects vertices. (Contributed by AV, 22-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑁 ∈ (0...(♯‘𝐹)) → (𝑃‘𝑁) ∈ 𝑉))
Theorem	wlkepvtx 29181	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘(♯‘𝐹)) ∈ 𝑉))
Theorem	wlkoniswlk 29182	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 29183	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 29184	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 29185	Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.)
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	wlkonl1iedg 29186*	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 29187	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 29188*	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 29189	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 29190	Lemma for wlkres 29191. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → 𝑆 ∈ V)
Theorem	wlkres 29191	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 29732. (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 29192	Lemma for redwlk 29193. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(♯‘𝐹))):(0...(♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))))⟶𝑉)
Theorem	redwlk 29193	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 29194	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    ⇒   ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃)
Theorem	wlkp1lem2 29195	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1))
Theorem	wlkp1lem3 29196	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    ⇒   ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
Theorem	wlkp1lem4 29197	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
Theorem	wlkp1lem5 29198*	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘))
Theorem	wlkp1lem6 29199*	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))))
Theorem	wlkp1lem7 29200	Lemma for wlkp1 29202. (Contributed by AV, 6-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))