Step | Hyp | Ref
| Expression |
1 | | clwwlkprop 26298 |
. . . . 5
⊢ (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉)) |
2 | | cshw0 13391 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 0) = 𝑊) |
3 | 2 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → (𝑊 cyclShift 0) = 𝑊) |
4 | 3 | eleq1d 2672 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → ((𝑊 cyclShift 0) ∈ (𝑉 ClWWalks 𝐸) ↔ 𝑊 ∈ (𝑉 ClWWalks 𝐸))) |
5 | 4 | biimprd 237 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑊 cyclShift 0) ∈ (𝑉 ClWWalks 𝐸))) |
6 | 1, 5 | mpcom 37 |
. . . 4
⊢ (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑊 cyclShift 0) ∈ (𝑉 ClWWalks 𝐸)) |
7 | | oveq2 6557 |
. . . . 5
⊢ (𝑁 = 0 → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift 0)) |
8 | 7 | eleq1d 2672 |
. . . 4
⊢ (𝑁 = 0 → ((𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 cyclShift 0) ∈ (𝑉 ClWWalks 𝐸))) |
9 | 6, 8 | syl5ibrcom 236 |
. . 3
⊢ (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑁 = 0 → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
10 | 9 | adantr 480 |
. 2
⊢ ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑁 = 0 → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
11 | | fzo1fzo0n0 12386 |
. . . . . 6
⊢ (𝑁 ∈ (1..^(#‘𝑊)) ↔ (𝑁 ∈ (0..^(#‘𝑊)) ∧ 𝑁 ≠ 0)) |
12 | | isclwwlk 26296 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
13 | 12 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) |
14 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
16 | | cshwcl 13395 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑁) ∈ Word 𝑉) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ Word 𝑉) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → (𝑊 cyclShift 𝑁) ∈ Word 𝑉) |
19 | 14 | anim1i 590 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊)))) |
20 | | 3simpc 1053 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) |
21 | | clwwisshclwwlem 26334 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸)) |
22 | 21 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸) |
23 | 19, 20, 22 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸) |
24 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ (1...(#‘𝑊))) |
25 | | lswcshw 13412 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1))) |
26 | 24, 25 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ( lastS ‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1))) |
27 | | fzo0ss1 12367 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1..^(#‘𝑊))
⊆ (0..^(#‘𝑊)) |
28 | 27 | sseli 3564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ (0..^(#‘𝑊))) |
29 | | cshwidx0 13403 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁)) |
30 | 28, 29 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁)) |
31 | 26, 30 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
32 | 31 | 3ad2antl3 1218 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
34 | | elfzo1 12385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ (1..^(#‘𝑊)) ↔ (𝑁 ∈ ℕ ∧ (#‘𝑊) ∈ ℕ ∧ 𝑁 < (#‘𝑊))) |
35 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
36 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℤ) |
37 | 35, 36 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ (𝑁 ∈ ℤ
∧ (#‘𝑊) ∈
ℤ)) |
38 | 37 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈
ℤ)) |
39 | 34, 38 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈
ℤ)) |
40 | | elfzom1b 12433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝑊) ∈ ℤ)
→ (𝑁 ∈
(1..^(#‘𝑊)) ↔
(𝑁 − 1) ∈
(0..^((#‘𝑊) −
1)))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑁 ∈ (1..^(#‘𝑊)) ↔ (𝑁 − 1) ∈ (0..^((#‘𝑊) − 1)))) |
42 | 41 | ibi 255 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑁 − 1) ∈ (0..^((#‘𝑊) − 1))) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑁 − 1) ∈ (0..^((#‘𝑊) − 1))) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (𝑁 − 1) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 1))) |
45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝑁 − 1))) |
46 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑁 − 1) → (𝑖 + 1) = ((𝑁 − 1) + 1)) |
47 | 46 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (𝑁 − 1) → (𝑊‘(𝑖 + 1)) = (𝑊‘((𝑁 − 1) + 1))) |
48 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ ℤ) |
49 | 48 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ ℂ) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → 𝑁 ∈ ℂ) |
51 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → 1 ∈
ℂ) |
52 | 50, 51 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑁 − 1) + 1) = 𝑁) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊‘((𝑁 − 1) + 1)) = (𝑊‘𝑁)) |
54 | 47, 53 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → (𝑊‘(𝑖 + 1)) = (𝑊‘𝑁)) |
55 | 45, 54 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)}) |
56 | 55 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑖 = (𝑁 − 1)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ ran 𝐸)) |
57 | 43, 56 | rspcdv 3285 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ ran 𝐸)) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 → (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ ran 𝐸)) |
59 | 58 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ ran 𝐸)) |
60 | 59 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → {(𝑊‘(𝑁 − 1)), (𝑊‘𝑁)} ∈ ran 𝐸) |
61 | 33, 60 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ ran 𝐸) |
62 | 18, 23, 61 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → ((𝑊 cyclShift 𝑁) ∈ Word 𝑉 ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ ran 𝐸)) |
63 | 62 | an32s 842 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁) ∈ Word 𝑉 ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ ran 𝐸)) |
64 | | 3simpa 1051 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
67 | | isclwwlk 26296 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 cyclShift 𝑁) ∈ Word 𝑉 ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ ran 𝐸))) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑊 cyclShift 𝑁) ∈ Word 𝑉 ∧ ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑊 cyclShift 𝑁)), ((𝑊 cyclShift 𝑁)‘0)} ∈ ran 𝐸))) |
69 | 63, 68 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)) |
70 | 69 | exp31 628 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → (𝑁 ∈ (1..^(#‘𝑊)) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)))) |
71 | 13, 70 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑊 ∈ Word 𝑉) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑁 ∈ (1..^(#‘𝑊)) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)))) |
72 | 1, 71 | mpcom 37 |
. . . . . . 7
⊢ (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑁 ∈ (1..^(#‘𝑊)) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
73 | 72 | com12 32 |
. . . . . 6
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
74 | 11, 73 | sylbir 224 |
. . . . 5
⊢ ((𝑁 ∈ (0..^(#‘𝑊)) ∧ 𝑁 ≠ 0) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
75 | 74 | expcom 450 |
. . . 4
⊢ (𝑁 ≠ 0 → (𝑁 ∈ (0..^(#‘𝑊)) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)))) |
76 | 75 | com13 86 |
. . 3
⊢ (𝑊 ∈ (𝑉 ClWWalks 𝐸) → (𝑁 ∈ (0..^(#‘𝑊)) → (𝑁 ≠ 0 → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)))) |
77 | 76 | imp 444 |
. 2
⊢ ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑁 ≠ 0 → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸))) |
78 | 10, 77 | pm2.61dne 2868 |
1
⊢ ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)) |