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 27124
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 26894. 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 27123 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3391 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1636 . . . . . 6 class 𝑤
6 c0 4116 . . . . . 6 class
75, 6wne 2978 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1636 . . . . . . . . 9 class 𝑖
109, 5cfv 6097 . . . . . . . 8 class (𝑤𝑖)
11 c1 10218 . . . . . . . . . 10 class 1
12 caddc 10220 . . . . . . . . . 10 class +
139, 11, 12co 6870 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6097 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4372 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1636 . . . . . . . 8 class 𝑔
17 cedg 26152 . . . . . . . 8 class Edg
1816, 17cfv 6097 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2156 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10217 . . . . . . 7 class 0
21 chash 13333 . . . . . . . . 9 class
225, 21cfv 6097 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10547 . . . . . . . 8 class
2422, 11, 23co 6870 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 12685 . . . . . . 7 class ..^
2620, 24, 25co 6870 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3096 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13499 . . . . . . . 8 class lastS
295, 28cfv 6097 . . . . . . 7 class (lastS‘𝑤)
3020, 5cfv 6097 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4372 . . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
3231, 18wcel 2156 . . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1100 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 26087 . . . . . 6 class Vtx
3516, 34cfv 6097 . . . . 5 class (Vtx‘𝑔)
3635cword 13498 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 3100 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 4923 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1637 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  27125
  Copyright terms: Public domain W3C validator