Metamath Proof Explorer

Definition df-wlks

Description: 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 ) discussed in Aksoy et al. The predicate F ( WalksG ) P can be read as "The pair <. F , P >. represents a walk in a graph G ", see also iswlk .

The condition { ( pk ) , ( p( k + 1 ) ) } C_ ( ( iEdgg )( fk ) ) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. ( pk ) = ( p( k + 1 ) ) should be allowed only if there is a loop at ( pk ) . Otherwise, C would be fulfilled by each edge containing ( pk ) .

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)

Ref Expression
Assertion df-wlks ⊢ Walks = g ∈ V ⟼ f p | f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwlks class Walks
1 vg setvar g
2 cvv class V
3 vf setvar f
4 vp setvar p
5 3 cv setvar f
6 ciedg class iEdg
7 1 cv setvar g
8 7 6 cfv class iEdg ⁡ g
9 8 cdm class dom ⁡ iEdg ⁡ g
10 9 cword class Word dom ⁡ iEdg ⁡ g
11 5 10 wcel wff f ∈ Word dom ⁡ iEdg ⁡ g
12 4 cv setvar p
13 cc0 class 0
14 cfz class …
15 chash class .
16 5 15 cfv class f
17 13 16 14 co class 0 … f
18 cvtx class Vtx
19 7 18 cfv class Vtx ⁡ g
20 17 19 12 wf wff p : 0 … f ⟶ Vtx ⁡ g
21 vk setvar k
22 cfzo class ..^
23 13 16 22 co class 0 ..^ f
24 21 cv setvar k
25 24 12 cfv class p ⁡ k
26 caddc class +
27 c1 class 1
28 24 27 26 co class k + 1
29 28 12 cfv class p ⁡ k + 1
30 25 29 wceq wff p ⁡ k = p ⁡ k + 1
31 24 5 cfv class f ⁡ k
32 31 8 cfv class iEdg ⁡ g ⁡ f ⁡ k
33 25 csn class p ⁡ k
34 32 33 wceq wff iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k
35 25 29 cpr class p ⁡ k p ⁡ k + 1
36 35 32 wss wff p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
37 30 34 36 wif wff if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
38 37 21 23 wral wff ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
39 11 20 38 w3a wff f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
40 39 3 4 copab class f p | f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
41 1 2 40 cmpt class g ∈ V ⟼ f p | f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k
42 0 41 wceq wff Walks = g ∈ V ⟼ f p | f ∈ Word dom ⁡ iEdg ⁡ g ∧ p : 0 … f ⟶ Vtx ⁡ g ∧ ∀ k ∈ 0 ..^ f if- p ⁡ k = p ⁡ k + 1 iEdg ⁡ g ⁡ f ⁡ k = p ⁡ k p ⁡ k p ⁡ k + 1 ⊆ iEdg ⁡ g ⁡ f ⁡ k