Proof of Theorem clwwisshclwwslem
Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12339 |
. . . . . . . . 9
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → 𝑁 ∈ ℤ) |
2 | | cshwlen 13396 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
3 | 1, 2 | sylan2 490 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
4 | 3 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((#‘(𝑊 cyclShift 𝑁)) − 1) = ((#‘𝑊) − 1)) |
5 | 4 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)) = (0..^((#‘𝑊) − 1))) |
6 | 5 | eleq2d 2673 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)) ↔ 𝑗 ∈ (0..^((#‘𝑊) − 1)))) |
7 | 6 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) → (𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)) ↔ 𝑗 ∈ (0..^((#‘𝑊) − 1)))) |
8 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → 𝑊 ∈ Word 𝑉) |
9 | 1 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → 𝑁 ∈ ℤ) |
10 | | lencl 13179 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
11 | | nn0z 11277 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℤ) |
12 | | peano2zm 11297 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℤ → ((#‘𝑊)
− 1) ∈ ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 1) ∈
ℤ) |
14 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
15 | 14 | lem1d 10836 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 1) ≤ (#‘𝑊)) |
16 | | eluz2 11569 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
(ℤ≥‘((#‘𝑊) − 1)) ↔ (((#‘𝑊) − 1) ∈ ℤ
∧ (#‘𝑊) ∈
ℤ ∧ ((#‘𝑊)
− 1) ≤ (#‘𝑊))) |
17 | 13, 11, 15, 16 | syl3anbrc 1239 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈
(ℤ≥‘((#‘𝑊) − 1))) |
18 | 10, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
(ℤ≥‘((#‘𝑊) − 1))) |
19 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈
(ℤ≥‘((#‘𝑊) − 1))) |
20 | | fzoss2 12365 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
(ℤ≥‘((#‘𝑊) − 1)) → (0..^((#‘𝑊) − 1)) ⊆
(0..^(#‘𝑊))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (0..^((#‘𝑊) − 1)) ⊆ (0..^(#‘𝑊))) |
22 | 21 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → 𝑗 ∈ (0..^(#‘𝑊))) |
23 | | cshwidxmod 13400 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑗 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝑗) = (𝑊‘((𝑗 + 𝑁) mod (#‘𝑊)))) |
24 | 8, 9, 22, 23 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → ((𝑊 cyclShift 𝑁)‘𝑗) = (𝑊‘((𝑗 + 𝑁) mod (#‘𝑊)))) |
25 | | elfzo1 12385 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ (1..^(#‘𝑊)) ↔ (𝑁 ∈ ℕ ∧ (#‘𝑊) ∈ ℕ ∧ 𝑁 < (#‘𝑊))) |
26 | 25 | simp2bi 1070 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
27 | 26 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → (#‘𝑊) ∈ ℕ) |
28 | | elfzom1p1elfzo 12414 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑗 ∈
(0..^((#‘𝑊) −
1))) → (𝑗 + 1) ∈
(0..^(#‘𝑊))) |
29 | 27, 28 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → (𝑗 + 1) ∈ (0..^(#‘𝑊))) |
30 | | cshwidxmod 13400 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑗 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(𝑗 + 1)) = (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))) |
31 | 8, 9, 29, 30 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → ((𝑊 cyclShift 𝑁)‘(𝑗 + 1)) = (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))) |
32 | 24, 31 | preq12d 4220 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → {((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} = {(𝑊‘((𝑗 + 𝑁) mod (#‘𝑊))), (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))}) |
33 | 32 | adantlr 747 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → {((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} = {(𝑊‘((𝑗 + 𝑁) mod (#‘𝑊))), (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))}) |
34 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 2 ∈
ℤ) |
36 | | nnz 11276 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℤ) |
37 | 36 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ∈
ℤ) |
38 | | nnnn0 11176 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℕ0) |
39 | 38 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ∈
ℕ0) |
40 | | nnne0 10930 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
≠ 0) |
41 | 40 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ≠ 0) |
42 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 1 ∈
ℝ) |
43 | | nnre 10904 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
44 | 43 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 𝑁 ∈ ℝ) |
45 | | nnre 10904 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ) |
46 | 45 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ∈
ℝ) |
47 | | nnge1 10923 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
48 | 47 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 1 ≤ 𝑁) |
49 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 𝑁 < (#‘𝑊)) |
50 | 42, 44, 46, 48, 49 | lelttrd 10074 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 1 < (#‘𝑊)) |
51 | 42, 50 | gtned 10051 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ≠ 1) |
52 | | nn0n0n1ge2 11235 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝑊) ≠ 0 ∧ (#‘𝑊) ≠ 1) → 2 ≤ (#‘𝑊)) |
53 | 39, 41, 51, 52 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → 2 ≤ (#‘𝑊)) |
54 | | eluz2 11569 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝑊) ∈ ℤ ∧ 2 ≤
(#‘𝑊))) |
55 | 35, 37, 53, 54 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊)) → (#‘𝑊) ∈
(ℤ≥‘2)) |
56 | 25, 55 | sylbi 206 |
. . . . . . . 8
⊢ (𝑁 ∈ (1..^(#‘𝑊)) → (#‘𝑊) ∈
(ℤ≥‘2)) |
57 | 56 | ad3antlr 763 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → (#‘𝑊) ∈
(ℤ≥‘2)) |
58 | | elfzoelz 12339 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^((#‘𝑊) − 1)) → 𝑗 ∈
ℤ) |
59 | 58 | adantl 481 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → 𝑗 ∈ ℤ) |
60 | 1 | ad3antlr 763 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → 𝑁 ∈ ℤ) |
61 | | simplrl 796 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) |
62 | | lsw 13204 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
64 | 63 | preq1d 4218 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {( lastS ‘𝑊), (𝑊‘0)} = {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)}) |
65 | 64 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ({( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸 ↔ {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸)) |
66 | 65 | biimpcd 238 |
. . . . . . . . . 10
⊢ ({( lastS
‘𝑊), (𝑊‘0)} ∈ 𝐸 → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸)) |
67 | 66 | adantl 481 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(0..^((#‘𝑊) −
1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸)) |
68 | 67 | impcom 445 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) → {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸) |
69 | 68 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸) |
70 | | clwwisshclwwlem1 26333 |
. . . . . . 7
⊢
((((#‘𝑊)
∈ (ℤ≥‘2) ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(𝑊‘((#‘𝑊) − 1)), (𝑊‘0)} ∈ 𝐸) → {(𝑊‘((𝑗 + 𝑁) mod (#‘𝑊))), (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))} ∈ 𝐸) |
71 | 57, 59, 60, 61, 69, 70 | syl311anc 1332 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → {(𝑊‘((𝑗 + 𝑁) mod (#‘𝑊))), (𝑊‘(((𝑗 + 1) + 𝑁) mod (#‘𝑊)))} ∈ 𝐸) |
72 | 33, 71 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) ∧ 𝑗 ∈ (0..^((#‘𝑊) − 1))) → {((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸) |
73 | 72 | ex 449 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) → (𝑗 ∈ (0..^((#‘𝑊) − 1)) → {((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸)) |
74 | 7, 73 | sylbid 229 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) → (𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)) → {((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸)) |
75 | 74 | ralrimiv 2948 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) ∧ (∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸)) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸) |
76 | 75 | ex 449 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸)) |