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 26279
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-clwlk 26278. 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.

Notice that by this definition, a single vertex cannot be represented as closed walk, since the word <" v "> with vertex v represents the walk "vv", which is a (closed) walk of length 1 (if there is an edge/loop from v to v). Therefore, a closed walk corresponds to a closed walk as word in an undirected graph only for walks of length at least 1, see clwlkisclwwlk2 26318. (Contributed by Alexander van der Vekens, 20-Mar-2018.)

Assertion
Ref Expression
df-clwwlk ClWWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)})
Distinct variable group:   𝑒,𝑖,𝑣,𝑤

Detailed syntax breakdown of Definition df-clwwlk
StepHypRef Expression
1 cclwwlk 26276 . 2 class ClWWalks
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 vi . . . . . . . . . 10 setvar 𝑖
65cv 1474 . . . . . . . . 9 class 𝑖
7 vw . . . . . . . . . 10 setvar 𝑤
87cv 1474 . . . . . . . . 9 class 𝑤
96, 8cfv 5804 . . . . . . . 8 class (𝑤𝑖)
10 c1 9816 . . . . . . . . . 10 class 1
11 caddc 9818 . . . . . . . . . 10 class +
126, 10, 11co 6549 . . . . . . . . 9 class (𝑖 + 1)
1312, 8cfv 5804 . . . . . . . 8 class (𝑤‘(𝑖 + 1))
149, 13cpr 4127 . . . . . . 7 class {(𝑤𝑖), (𝑤‘(𝑖 + 1))}
153cv 1474 . . . . . . . 8 class 𝑒
1615crn 5039 . . . . . . 7 class ran 𝑒
1714, 16wcel 1977 . . . . . 6 wff {(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
18 cc0 9815 . . . . . . 7 class 0
19 chash 12979 . . . . . . . . 9 class #
208, 19cfv 5804 . . . . . . . 8 class (#‘𝑤)
21 cmin 10145 . . . . . . . 8 class
2220, 10, 21co 6549 . . . . . . 7 class ((#‘𝑤) − 1)
23 cfzo 12334 . . . . . . 7 class ..^
2418, 22, 23co 6549 . . . . . 6 class (0..^((#‘𝑤) − 1))
2517, 5, 24wral 2896 . . . . 5 wff 𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
26 clsw 13147 . . . . . . . 8 class lastS
278, 26cfv 5804 . . . . . . 7 class ( lastS ‘𝑤)
2818, 8cfv 5804 . . . . . . 7 class (𝑤‘0)
2927, 28cpr 4127 . . . . . 6 class {( lastS ‘𝑤), (𝑤‘0)}
3029, 16wcel 1977 . . . . 5 wff {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒
3125, 30wa 383 . . . 4 wff (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)
322cv 1474 . . . . 5 class 𝑣
3332cword 13146 . . . 4 class Word 𝑣
3431, 7, 33crab 2900 . . 3 class {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)}
352, 3, 4, 4, 34cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)})
361, 35wceq 1475 1 wff ClWWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  clwwlk  26294  clwwlkprop  26298
  Copyright terms: Public domain W3C validator