MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clwwlk Structured version   Visualization version   GIF version

Definition df-clwwlk 27127
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 26899. 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.)
Assertion
Ref Expression
df-clwwlk ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
Distinct variable group:   𝑔,𝑖,𝑤

Detailed syntax breakdown of Definition df-clwwlk
StepHypRef Expression
1 cclwwlk 27126 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3341 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1631 . . . . . 6 class 𝑤
6 c0 4059 . . . . . 6 class
75, 6wne 2933 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1631 . . . . . . . . 9 class 𝑖
109, 5cfv 6050 . . . . . . . 8 class (𝑤𝑖)
11 c1 10150 . . . . . . . . . 10 class 1
12 caddc 10152 . . . . . . . . . 10 class +
139, 11, 12co 6815 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6050 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4324 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1631 . . . . . . . 8 class 𝑔
17 cedg 26160 . . . . . . . 8 class Edg
1816, 17cfv 6050 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2140 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10149 . . . . . . 7 class 0
21 chash 13332 . . . . . . . . 9 class
225, 21cfv 6050 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10479 . . . . . . . 8 class
2422, 11, 23co 6815 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 12680 . . . . . . 7 class ..^
2620, 24, 25co 6815 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3051 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13499 . . . . . . . 8 class lastS
295, 28cfv 6050 . . . . . . 7 class (lastS‘𝑤)
3020, 5cfv 6050 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4324 . . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
3231, 18wcel 2140 . . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1072 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 26095 . . . . . 6 class Vtx
3516, 34cfv 6050 . . . . 5 class (Vtx‘𝑔)
3635cword 13498 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 3055 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 4882 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1632 1 wff ClWWalks = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlk  27128
  Copyright terms: Public domain W3C validator