MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clwwlks Structured version   Visualization version   GIF version

Definition df-clwwlks 26858
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 26648. 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 26856 . 2 class ClWWalks
2 vg . . 3 setvar 𝑔
3 cvv 3195 . . 3 class V
4 vw . . . . . . 7 setvar 𝑤
54cv 1480 . . . . . 6 class 𝑤
6 c0 3907 . . . . . 6 class
75, 6wne 2791 . . . . 5 wff 𝑤 ≠ ∅
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1480 . . . . . . . . 9 class 𝑖
109, 5cfv 5876 . . . . . . . 8 class (𝑤𝑖)
11 c1 9922 . . . . . . . . . 10 class 1
12 caddc 9924 . . . . . . . . . 10 class +
139, 11, 12co 6635 . . . . . . . . 9 class (𝑖 + 1)
1413, 5cfv 5876 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
1510, 14cpr 4170 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
162cv 1480 . . . . . . . 8 class 𝑔
17 cedg 25920 . . . . . . . 8 class Edg
1816, 17cfv 5876 . . . . . . 7 class (Edg‘𝑔)
1915, 18wcel 1988 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
20 cc0 9921 . . . . . . 7 class 0
21 chash 13100 . . . . . . . . 9 class #
225, 21cfv 5876 . . . . . . . 8 class (#‘𝑤)
23 cmin 10251 . . . . . . . 8 class
2422, 11, 23co 6635 . . . . . . 7 class ((#‘𝑤) − 1)
25 cfzo 12449 . . . . . . 7 class ..^
2620, 24, 25co 6635 . . . . . 6 class (0..^((#‘𝑤) − 1))
2719, 8, 26wral 2909 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔)
28 clsw 13275 . . . . . . . 8 class lastS
295, 28cfv 5876 . . . . . . 7 class ( lastS ‘𝑤)
3020, 5cfv 5876 . . . . . . 7 class (𝑤‘0)
3129, 30cpr 4170 . . . . . 6 class {( lastS ‘𝑤), (𝑤‘0)}
3231, 18wcel 1988 . . . . 5 wff {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔)
337, 27, 32w3a 1036 . . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))
34 cvtx 25855 . . . . . 6 class Vtx
3516, 34cfv 5876 . . . . 5 class (Vtx‘𝑔)
3635cword 13274 . . . 4 class Word (Vtx‘𝑔)
3733, 4, 36crab 2913 . . 3 class {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))}
382, 3, 37cmpt 4720 . 2 class (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔) ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ (Edg‘𝑔))})
391, 38wceq 1481 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  26860
  Copyright terms: Public domain W3C validator