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 30001
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 29791. 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 30000 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3480 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1539 . . . . . 6 class 𝑤
6 c0 4333 . . . . . 6 class
75, 6wne 2940 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1539 . . . . . . . . 9 class 𝑖
109, 5cfv 6561 . . . . . . . 8 class (𝑤𝑖)
11 c1 11156 . . . . . . . . . 10 class 1
12 caddc 11158 . . . . . . . . . 10 class +
139, 11, 12co 7431 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6561 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4628 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1539 . . . . . . . 8 class 𝑔
17 cedg 29064 . . . . . . . 8 class Edg
1816, 17cfv 6561 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2108 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 11155 . . . . . . 7 class 0
21 chash 14369 . . . . . . . . 9 class
225, 21cfv 6561 . . . . . . . 8 class (♯‘𝑤)
23 cmin 11492 . . . . . . . 8 class
2422, 11, 23co 7431 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 13694 . . . . . . 7 class ..^
2620, 24, 25co 7431 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3061 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 14600 . . . . . . . 8 class lastS
295, 28cfv 6561 . . . . . . 7 class (lastS‘𝑤)
3020, 5cfv 6561 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4628 . . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
3231, 18wcel 2108 . . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1087 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 29013 . . . . . 6 class Vtx
3516, 34cfv 6561 . . . . 5 class (Vtx‘𝑔)
3635cword 14552 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 3436 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 5225 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1540 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  30002
  Copyright terms: Public domain W3C validator