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 27674
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 27466. 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 27673 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3500 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1529 . . . . . 6 class 𝑤
6 c0 4295 . . . . . 6 class
75, 6wne 3021 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1529 . . . . . . . . 9 class 𝑖
109, 5cfv 6352 . . . . . . . 8 class (𝑤𝑖)
11 c1 10527 . . . . . . . . . 10 class 1
12 caddc 10529 . . . . . . . . . 10 class +
139, 11, 12co 7148 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 6352 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4566 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1529 . . . . . . . 8 class 𝑔
17 cedg 26746 . . . . . . . 8 class Edg
1816, 17cfv 6352 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 2107 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 10526 . . . . . . 7 class 0
21 chash 13680 . . . . . . . . 9 class
225, 21cfv 6352 . . . . . . . 8 class (♯‘𝑤)
23 cmin 10859 . . . . . . . 8 class
2422, 11, 23co 7148 . . . . . . 7 class ((♯‘𝑤) − 1)
25 cfzo 13023 . . . . . . 7 class ..^
2620, 24, 25co 7148 . . . . . 6 class (0..^((♯‘𝑤) − 1))
2719, 8, 26wral 3143 . . . . 5 wff 𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13904 . . . . . . . 8 class lastS
295, 28cfv 6352 . . . . . . 7 class (lastS‘𝑤)
3020, 5cfv 6352 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4566 . . . . . 6 class {(lastS‘𝑤), (𝑤‘0)}
3231, 18wcel 2107 . . . . 5 wff {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1081 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 26695 . . . . . 6 class Vtx
3516, 34cfv 6352 . . . . 5 class (Vtx‘𝑔)
3635cword 13851 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 3147 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 5143 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {(lastS‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1530 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  27675
  Copyright terms: Public domain W3C validator