Users' Mathboxes 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 41183
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 40975. 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 41181 . 2 class ClWWalkS
2 vg . . 3 setvar 𝑔
3 cvv 3168 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1473 . . . . . 6 class 𝑤
6 c0 3869 . . . . . 6 class
75, 6wne 2775 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1473 . . . . . . . . 9 class 𝑖
109, 5cfv 5786 . . . . . . . 8 class (𝑤𝑖)
11 c1 9789 . . . . . . . . . 10 class 1
12 caddc 9791 . . . . . . . . . 10 class +
139, 11, 12co 6523 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 5786 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4122 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1473 . . . . . . . 8 class 𝑔
17 cedga 40349 . . . . . . . 8 class Edg
1816, 17cfv 5786 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 1975 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 9788 . . . . . . 7 class 0
21 chash 12930 . . . . . . . . 9 class #
225, 21cfv 5786 . . . . . . . 8 class (#‘𝑤)
23 cmin 10113 . . . . . . . 8 class
2422, 11, 23co 6523 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12285 . . . . . . 7 class ..^
2620, 24, 25co 6523 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 8, 26wral 2891 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13089 . . . . . . . 8 class lastS
295, 28cfv 5786 . . . . . . 7 class ( lastS ‘𝑤)
3020, 5cfv 5786 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4122 . . . . . 6 class {( lastS ‘𝑤), (𝑤‘0)}
3231, 18wcel 1975 . . . . 5 wff {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1030 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 40227 . . . . . 6 class Vtx
3516, 34cfv 5786 . . . . 5 class (Vtx‘𝑔)
3635cword 13088 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 2895 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 4633 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1474 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  41185
  Copyright terms: Public domain W3C validator