Metamath Proof Explorer

Definition df-clwwlk

Description: Define the set of all closed walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks . Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Assertion df-clwwlk ⊢ ClWWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwwlk class ClWWalks
1 vg setvar g
2 cvv class V
3 vw setvar w
4 cvtx class Vtx
5 1 cv setvar g
6 5 4 cfv class Vtx ⁡ g
7 6 cword class Word Vtx ⁡ g
8 3 cv setvar w
9 c0 class ∅
10 8 9 wne wff w ≠ ∅
11 vi setvar i
12 cc0 class 0
13 cfzo class ..^
14 chash class .
15 8 14 cfv class w
16 cmin class −
17 c1 class 1
18 15 17 16 co class w − 1
19 12 18 13 co class 0 ..^ w − 1
20 11 cv setvar i
21 20 8 cfv class w ⁡ i
22 caddc class +
23 20 17 22 co class i + 1
24 23 8 cfv class w ⁡ i + 1
25 21 24 cpr class w ⁡ i w ⁡ i + 1
26 cedg class Edg
27 5 26 cfv class Edg ⁡ g
28 25 27 wcel wff w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
29 28 11 19 wral wff ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g
30 clsw class lastS
31 8 30 cfv class lastS ⁡ w
32 12 8 cfv class w ⁡ 0
33 31 32 cpr class lastS ⁡ w w ⁡ 0
34 33 27 wcel wff lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g
35 10 29 34 w3a wff w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g
36 35 3 7 crab class w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g
37 1 2 36 cmpt class g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g
38 0 37 wceq wff ClWWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g