Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | clwwlkbp 26883 |
. . . . 5
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅)) |
3 | | cshw0 13540 |
. . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 cyclShift 0) = 𝑊) |
4 | 3 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (𝑊 cyclShift 0) = 𝑊) |
5 | 4 | eleq1d 2686 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → ((𝑊 cyclShift 0) ∈ (ClWWalks‘𝐺) ↔ 𝑊 ∈ (ClWWalks‘𝐺))) |
6 | 5 | biimprd 238 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) → (𝑊 cyclShift 0) ∈ (ClWWalks‘𝐺))) |
7 | 2, 6 | mpcom 38 |
. . . 4
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → (𝑊 cyclShift 0) ∈ (ClWWalks‘𝐺)) |
8 | | oveq2 6658 |
. . . . 5
⊢ (𝑁 = 0 → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift 0)) |
9 | 8 | eleq1d 2686 |
. . . 4
⊢ (𝑁 = 0 → ((𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺) ↔ (𝑊 cyclShift 0) ∈ (ClWWalks‘𝐺))) |
10 | 7, 9 | syl5ibrcom 237 |
. . 3
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → (𝑁 = 0 → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺))) |
11 | 10 | adantr 481 |
. 2
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑁 = 0 → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺))) |
12 | | fzo1fzo0n0 12518 |
. . . . . 6
⊢ (𝑁 ∈ (1..^(#‘𝑊)) ↔ (𝑁 ∈ (0..^(#‘𝑊)) ∧ 𝑁 ≠ 0)) |
13 | | cshwcl 13544 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺)) |
14 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺)) |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺)) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺)) |
17 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word (Vtx‘𝐺)) |
18 | | elfzoelz 12470 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ ℤ) |
19 | | cshwlen 13545 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
20 | 17, 18, 19 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
21 | | hasheq0 13154 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((#‘𝑊) = 0 ↔ 𝑊 = ∅)) |
22 | 21 | bicomd 213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 = ∅ ↔ (#‘𝑊) = 0)) |
23 | 22 | necon3bid 2838 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 ≠ ∅ ↔ (#‘𝑊) ≠ 0)) |
24 | 23 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (#‘𝑊) ≠ 0) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ≠ 0) |
26 | 20, 25 | eqnetrd 2861 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘(𝑊 cyclShift 𝑁)) ≠ 0) |
27 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺)) |
28 | | hasheq0 13154 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺) → ((#‘(𝑊 cyclShift 𝑁)) = 0 ↔ (𝑊 cyclShift 𝑁) = ∅)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((#‘(𝑊 cyclShift 𝑁)) = 0 ↔ (𝑊 cyclShift 𝑁) = ∅)) |
30 | 29 | necon3bid 2838 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((#‘(𝑊 cyclShift 𝑁)) ≠ 0 ↔ (𝑊 cyclShift 𝑁) ≠ ∅)) |
31 | 26, 30 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ≠ ∅) |
32 | 31 | 3ad2antl1 1223 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ≠ ∅) |
33 | 16, 32 | jca 554 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 cyclShift 𝑁) ≠ ∅)) |
34 | 17 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
35 | 34 | anim1i 592 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊)))) |
36 | | 3simpc 1060 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
37 | 36 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
38 | | clwwisshclwwslem 26927 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ (Edg‘𝐺))) |
39 | 35, 37, 38 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ (Edg‘𝐺)) |
40 | | elfzofz 12485 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ (1...(#‘𝑊))) |
41 | | lswcshw 13561 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1))) |
42 | 40, 41 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ( lastS ‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1))) |
43 | | fzo0ss1 12498 |
. . . . . . . . . . . . . . . . 17
⊢
(1..^(#‘𝑊))
⊆ (0..^(#‘𝑊)) |
44 | 43 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ (0..^(#‘𝑊))) |
45 | | cshwidx0 13552 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁)) |
46 | 44, 45 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁)) |
47 | 42, 46 | preq12d 4276 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
48 | 47 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑁 ∈ (1..^(#‘𝑊)) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)})) |
49 | 48 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (𝑁 ∈ (1..^(#‘𝑊)) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)})) |
50 | 49 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑁 ∈ (1..^(#‘𝑊)) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)})) |
51 | 50 | imp 445 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
52 | | elfzo1elm1fzo0 12569 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑁 − 1) ∈ (0..^((#‘𝑊) − 1))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑁 − 1) ∈ (0..^((#‘𝑊) − 1))) |
54 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑁 − 1) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 1))) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 1))) |
56 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
57 | 56 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑁 − 1) → (𝑊‘(𝑖 + 1)) = (𝑊‘((𝑁 − 1) + 1))) |
58 | 18 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ ℂ) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → 𝑁 ∈ ℂ) |
60 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → 1 ∈
ℂ) |
61 | 59, 60 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑁 − 1) + 1) = 𝑁) |
62 | 61 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊‘((𝑁 − 1) + 1)) = (𝑊‘𝑁)) |
63 | 57, 62 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊‘𝑁)) |
64 | 55, 63 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
65 | 64 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))) |
66 | 53, 65 | rspcdv 3312 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))) |
67 | 66 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)))) |
68 | 67 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑁 ∈ (1..^(#‘𝑊)) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))))) |
69 | 68 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (𝑁 ∈ (1..^(#‘𝑊)) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))))) |
70 | 69 | com24 95 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺) → (𝑁 ∈ (1..^(#‘𝑊)) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺))))) |
71 | 70 | 3imp1 1280 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ (Edg‘𝐺)) |
72 | 51, 71 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ (Edg‘𝐺)) |
73 | 33, 39, 72 | 3jca 1242 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (((𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 cyclShift 𝑁) ≠ ∅) ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ (Edg‘𝐺))) |
74 | 73 | expcom 451 |
. . . . . . 7
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) → (((𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 cyclShift 𝑁) ≠ ∅) ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ (Edg‘𝐺)))) |
75 | | eqid 2622 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
76 | 1, 75 | isclwwlks 26880 |
. . . . . . 7
⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
77 | 1, 75 | isclwwlks 26880 |
. . . . . . 7
⊢ ((𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺) ↔ (((𝑊 cyclShift 𝑁) ∈ Word (Vtx‘𝐺) ∧ (𝑊 cyclShift 𝑁) ≠ ∅) ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ (Edg‘𝐺))) |
78 | 74, 76, 77 | 3imtr4g 285 |
. . . . . 6
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑊 ∈ (ClWWalks‘𝐺) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺))) |
79 | 12, 78 | sylbir 225 |
. . . . 5
⊢ ((𝑁 ∈ (0..^(#‘𝑊)) ∧ 𝑁 ≠ 0) → (𝑊 ∈ (ClWWalks‘𝐺) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺))) |
80 | 79 | expcom 451 |
. . . 4
⊢ (𝑁 ≠ 0 → (𝑁 ∈ (0..^(#‘𝑊)) → (𝑊 ∈ (ClWWalks‘𝐺) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺)))) |
81 | 80 | com13 88 |
. . 3
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → (𝑁 ∈ (0..^(#‘𝑊)) → (𝑁 ≠ 0 → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺)))) |
82 | 81 | imp 445 |
. 2
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑁 ≠ 0 → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺))) |
83 | 11, 82 | pm2.61dne 2880 |
1
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺)) |