Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-clwwlks Structured version   Visualization version   GIF version

Definition df-clwwlks 41185
 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 40977. 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-clwwlks ClWWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
Distinct variable group:   𝑔,𝑖,𝑤

Detailed syntax breakdown of Definition df-clwwlks
StepHypRef Expression
1 cclwwlks 41183 . 2 class ClWWalkS
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1474 . . . . . 6 class 𝑤
6 c0 3874 . . . . . 6 class
75, 6wne 2780 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1474 . . . . . . . . 9 class 𝑖
109, 5cfv 5804 . . . . . . . 8 class (𝑤𝑖)
11 c1 9816 . . . . . . . . . 10 class 1
12 caddc 9818 . . . . . . . . . 10 class +
139, 11, 12co 6549 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 5804 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4127 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1474 . . . . . . . 8 class 𝑔
17 cedga 25792 . . . . . . . 8 class Edg
1816, 17cfv 5804 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 1977 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 9815 . . . . . . 7 class 0
21 chash 12979 . . . . . . . . 9 class #
225, 21cfv 5804 . . . . . . . 8 class (#‘𝑤)
23 cmin 10145 . . . . . . . 8 class
2422, 11, 23co 6549 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12334 . . . . . . 7 class ..^
2620, 24, 25co 6549 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 8, 26wral 2896 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13147 . . . . . . . 8 class lastS
295, 28cfv 5804 . . . . . . 7 class ( lastS ‘𝑤)
3020, 5cfv 5804 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4127 . . . . . 6 class {( lastS ‘𝑤), (𝑤‘0)}
3231, 18wcel 1977 . . . . 5 wff {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1031 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 25673 . . . . . 6 class Vtx
3516, 34cfv 5804 . . . . 5 class (Vtx‘𝑔)
3635cword 13146 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 2900 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 4643 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1475 1 wff ClWWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
 Colors of variables: wff setvar class This definition is referenced by:  clwwlks  41187
 Copyright terms: Public domain W3C validator