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 29202
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 28995. 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 29201 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3475 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1541 . . . . . 6 class 𝑤
6 c0 4320 . . . . . 6 class
75, 6wne 2941 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1541 . . . . . . . . 9 class 𝑖
109, 5cfv 6535 . . . . . . . 8 class (𝑤𝑖)
11 c1 11098 . . . . . . . . . 10 class 1
12 caddc 11100 . . . . . . . . . 10 class +
139, 11, 12co 7396 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6535 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4626 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1541 . . . . . . . 8 class 𝑔
17 cedg 28274 . . . . . . . 8 class Edg
1816, 17cfv 6535 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2107 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 11097 . . . . . . 7 class 0
21 chash 14277 . . . . . . . . 9 class
225, 21cfv 6535 . . . . . . . 8 class (♯‘𝑤)
23 cmin 11431 . . . . . . . 8 class
2422, 11, 23co 7396 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 13614 . . . . . . 7 class ..^
2620, 24, 25co 7396 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3062 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 14499 . . . . . . . 8 class lastS
295, 28cfv 6535 . . . . . . 7 class (lastS‘𝑤)
3020, 5cfv 6535 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4626 . . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
3231, 18wcel 2107 . . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1088 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 28223 . . . . . 6 class Vtx
3516, 34cfv 6535 . . . . 5 class (Vtx‘𝑔)
3635cword 14451 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 3433 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 5227 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1542 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  29203
  Copyright terms: Public domain W3C validator