P. 296 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29501-29600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uhgr0edg0rgr 29501	A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Edg‘𝐺) = ∅) → 𝐺 RegGraph 0)
Theorem	uhgr0edg0rgrb 29502	A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.)
⊢ (𝐺 ∈ UHGraph → (𝐺 RegGraph 0 ↔ (Edg‘𝐺) = ∅))
Theorem	usgr0edg0rusgr 29503	A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 19-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
⊢ (𝐺 ∈ USGraph → (𝐺 RegUSGraph 0 ↔ (Edg‘𝐺) = ∅))
Theorem	0vtxrgr 29504*	A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘)
Theorem	0vtxrusgr 29505*	A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘)
Theorem	0uhgrrusgr 29506*	The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘)
Theorem	0grrusgr 29507	The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020.)
⊢ ∀𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘
Theorem	0grrgr 29508	The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.)
⊢ ∀𝑘 ∈ ℕ0* ∅ RegGraph 𝑘
Theorem	cusgrrusgr 29509	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 29510	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 29511*	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 29512*	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 29513*	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 29514*	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 29515*	Lemma for rusgr1vtx 29516. (Contributed by AV, 27-Dec-2020.)
⊢ (((∀𝑣 ∈ 𝑉 (♯‘𝐴) = 𝐾 ∧ ∀𝑣 ∈ 𝑉 𝐴 = ∅) ∧ (𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 1)) → 𝐾 = 0)
Theorem	rusgr1vtx 29516	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 29517*	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∈ USGraph ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rusgrprc 29518	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegUSGraph 0} ∉ V
Theorem	rgrprc 29519	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegGraph 0} ∉ V
Theorem	rgrprcx 29520*	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rgrx0ndm 29521*	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 29522*	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 29527. 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 29620): 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 29644): 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 29645): 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 29701): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n). * Circuits (df-crcts 29716): "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 29717): 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 30127): 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 3950 and elopabran 5522 to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk 29704, see clwlkwlk 29705 and clwlkswks 29706): * Trails are walks (trliswlk 29625): (Trails‘𝐺) ⊆ (Walks‘𝐺) * Paths are trails (pthistrl 29653): (Paths‘𝐺) ⊆ (Trails‘𝐺) * Simple paths are paths (spthispth 29654): (SPaths‘𝐺) ⊆ (Paths‘𝐺) * Closed walks are walks (clwlkiswlk 29704): (ClWalks‘𝐺) ⊆ (Walks‘𝐺) * Circuits are closed walks (crctisclwlk 29724): (Circuits‘𝐺) ⊆ (ClWalks‘𝐺) * Circuits are trails (crctistrl 29725): (Circuits‘𝐺) ⊆ (Trails‘𝐺) * Cycles are paths (cyclispth 29727): (Cycles‘𝐺) ⊆ (Paths‘𝐺) * Cycles are circuits (cycliscrct 29729): (Cycles‘𝐺) ⊆ (Circuits‘𝐺) * (Non-trivial) cycles are not simple paths (cyclnspth 29731): (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃)) * Eulerian paths are trails (eupthistrl 30140): (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 14479, 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 29760 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 29806. 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 29761): n = N * WSPathsN (simple paths of length N as word, df-wspthsn 29763): p(i) =/= p(j) if i =/= j and n = N * ClWWalks (closed walks as word, df-clwwlk 29911): p(0) = p(n) * ClWWalksN (closed walks of length N as word, df-clwwlkn 29954): 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 29528): 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 * Trails with particular endpoints (df-trlson 29621): 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 * Paths with particular endpoints (df-pthson 29646): 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 * Simple paths with particular endpoints (df-spthson 29647): 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 * Walks of a fixed length 𝑁 as words with particular endpoints (df-wwlksnon 29762): (𝐴(𝑁 WWalksNOn 𝐺)𝐵) * Simple paths of a fixed length 𝑁 as words with particular endpoints (df-wspthsnon 29764): (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) * Closed Walks of a fixed length 𝑁 as words anchored at a particular vertex 𝐴 (df-wwlksnon 29762): (𝐴(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 29526. 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 29527, restricting s to 1. wlk1ewlk 29568 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level".
Syntax	cewlks 29523	Extend class notation with s-walks "on the edge level" (of a hypergraph).
class EdgWalks
Syntax	cwlks 29524	Extend class notation with walks (i.e. 1-walks) (of a hypergraph).
class Walks
Syntax	cwlkson 29525	Extend class notation with walks between two vertices (within a graph).
class WalksOn
Definition	df-ewlks 29526*	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 29527*	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 29567) discussed in Aksoy et al. The predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk in a graph 𝐺", see also iswlk 29538. 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 29528*	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 29585. 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 29529*	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 29530*	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 29531*	Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))
Theorem	ewlkinedg 29532	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 29533	An s-walk of edges is also a t-walk of edges if 𝑡 ≤ 𝑠. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇))
Theorem	upgrewlkle2 29534	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 29535	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 29536	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 29537*	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 29538*	Properties of a pair of functions to be/represent a walk. (Contributed by AV, 30-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
Theorem	wlkprop 29539*	Properties of a walk. (Contributed by AV, 5-Nov-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
Theorem	wlkv 29540	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 29541*	Generalization of iswlk 29538: 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 29542	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 29543	A walk has length ♯(𝐹), which is an integer. Formerly proven for an Eulerian path, see eupthcl 30139. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0)
Theorem	wlkp 29544	The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
Theorem	wlkpwrd 29545	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 29546	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 29547*	The class of walks is a set. (Contributed by AV, 15-Jan-2021.) (Proof shortened by SN, 11-Dec-2024.)
⊢ {⟨𝑓, 𝑝⟩ ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V
Theorem	wksvOLD 29548*	Obsolete version of wksv 29547 as of 11-Dec-2024. (Contributed by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {⟨𝑓, 𝑝⟩ ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V
Theorem	wlkn0 29549	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 29550	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 29551	Lemma for wlkvtxeledg 29552: 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 29552*	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 29553*	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 29554	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 29555	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 29556	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 29557	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 29558*	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 29559*	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 29560*	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 29561	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 29562*	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 29563	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 29564	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 29565	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 29566	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 29567*	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 29568	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 29569*	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 29570*	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 29571*	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 29572*	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 29573*	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 29574*	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 29575	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 29576	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 29577*	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 29578*	Obsolete version of opabresex2 7441 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 29579	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 29580	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 29581	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 29582	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 29583	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 29584*	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 29585	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 29586	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 29587	A walk connects vertices. (Contributed by AV, 22-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑁 ∈ (0...(♯‘𝐹)) → (𝑃‘𝑁) ∈ 𝑉))
Theorem	wlkepvtx 29588	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘(♯‘𝐹)) ∈ 𝑉))
Theorem	wlkoniswlk 29589	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 29590	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 29591	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 29592	Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.)
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	wlkonl1iedg 29593*	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 29594	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 29595*	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 29596	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 29597	Lemma for wlkres 29598. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)    ⇒   ⊢ (𝜑 → 𝑆 ∈ V)
Theorem	wlkres 29598	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 30144. (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 29599	Lemma for redwlk 29600. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(♯‘𝐹))):(0...(♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))))⟶𝑉)
Theorem	redwlk 29600	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..^(♯‘𝐹))))