Description: Define the set of all walks (in a pseudograph), called "simple walks" in the following.
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory) , 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)."
According to Bollobas: " A walk W in a graph is an alternating sequence
of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) =
x(i-1)x(i), 0
Therefore, 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).
Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudographs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017) (Revised by AV, 28-Dec-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-upwlks | ⊢ UPWalks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cupwlks | ⊢ UPWalks | |
| 1 | vg | ⊢ 𝑔 | |
| 2 | cvv | ⊢ V | |
| 3 | vf | ⊢ 𝑓 | |
| 4 | vp | ⊢ 𝑝 | |
| 5 | 3 | cv | ⊢ 𝑓 |
| 6 | ciedg | ⊢ iEdg | |
| 7 | 1 | cv | ⊢ 𝑔 |
| 8 | 7 6 | cfv | ⊢ ( iEdg ‘ 𝑔 ) |
| 9 | 8 | cdm | ⊢ dom ( iEdg ‘ 𝑔 ) |
| 10 | 9 | cword | ⊢ Word dom ( iEdg ‘ 𝑔 ) |
| 11 | 5 10 | wcel | ⊢ 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) |
| 12 | 4 | cv | ⊢ 𝑝 |
| 13 | cc0 | ⊢ 0 | |
| 14 | cfz | ⊢ ... | |
| 15 | chash | ⊢ ♯ | |
| 16 | 5 15 | cfv | ⊢ ( ♯ ‘ 𝑓 ) |
| 17 | 13 16 14 | co | ⊢ ( 0 ... ( ♯ ‘ 𝑓 ) ) |
| 18 | cvtx | ⊢ Vtx | |
| 19 | 7 18 | cfv | ⊢ ( Vtx ‘ 𝑔 ) |
| 20 | 17 19 12 | wf | ⊢ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) |
| 21 | vk | ⊢ 𝑘 | |
| 22 | cfzo | ⊢ ..^ | |
| 23 | 13 16 22 | co | ⊢ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) |
| 24 | 21 | cv | ⊢ 𝑘 |
| 25 | 24 5 | cfv | ⊢ ( 𝑓 ‘ 𝑘 ) |
| 26 | 25 8 | cfv | ⊢ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) |
| 27 | 24 12 | cfv | ⊢ ( 𝑝 ‘ 𝑘 ) |
| 28 | caddc | ⊢ + | |
| 29 | c1 | ⊢ 1 | |
| 30 | 24 29 28 | co | ⊢ ( 𝑘 + 1 ) |
| 31 | 30 12 | cfv | ⊢ ( 𝑝 ‘ ( 𝑘 + 1 ) ) |
| 32 | 27 31 | cpr | ⊢ { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } |
| 33 | 26 32 | wceq | ⊢ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } |
| 34 | 33 21 23 | wral | ⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } |
| 35 | 11 20 34 | w3a | ⊢ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) |
| 36 | 35 3 4 | copab | ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } |
| 37 | 1 2 36 | cmpt | ⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) |
| 38 | 0 37 | wceq | ⊢ UPWalks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) |