Step | Hyp | Ref
| Expression |
1 | | cshwlen 13396 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑀)) = (#‘𝑊)) |
2 | 1 | 3adant3 1074 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑀)) = (#‘𝑊)) |
3 | | cshwcl 13395 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
4 | 3 | anim1i 590 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) |
5 | 4 | 3adant2 1073 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) |
6 | | cshwlen 13396 |
. . . . 5
⊢ (((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift 𝑀))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift 𝑀))) |
8 | | simp1 1054 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑊 ∈ Word 𝑉) |
9 | | zaddcl 11294 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
10 | 9 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
11 | 8, 10 | jca 553 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝑁) ∈ ℤ)) |
12 | | cshwlen 13396 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝑁) ∈ ℤ) → (#‘(𝑊 cyclShift (𝑀 + 𝑁))) = (#‘𝑊)) |
13 | 11, 12 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift (𝑀 + 𝑁))) = (#‘𝑊)) |
14 | 2, 7, 13 | 3eqtr4d 2654 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift (𝑀 + 𝑁)))) |
15 | 7, 2 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘𝑊)) |
16 | 15 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(0..^(#‘((𝑊 cyclShift
𝑀) cyclShift 𝑁))) = (0..^(#‘𝑊))) |
17 | 16 | eleq2d 2673 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁))) ↔ 𝑖 ∈ (0..^(#‘𝑊)))) |
18 | 3 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
20 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑁 ∈ ℤ) |
22 | 2 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (#‘𝑊) = (#‘(𝑊 cyclShift 𝑀))) |
23 | 22 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^(#‘𝑊)) = (0..^(#‘(𝑊 cyclShift 𝑀)))) |
24 | 23 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝑊)) ↔ 𝑖 ∈ (0..^(#‘(𝑊 cyclShift 𝑀))))) |
25 | 24 | biimpa 500 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘(𝑊 cyclShift 𝑀)))) |
26 | | cshwidxmod 13400 |
. . . . . . . 8
⊢ (((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘(𝑊 cyclShift 𝑀)))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))))) |
27 | 19, 21, 25, 26 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))))) |
28 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
29 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑀 ∈ ℤ) |
30 | | elfzo0 12376 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^(#‘𝑊)) ↔ (𝑖 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝑖 < (#‘𝑊))) |
31 | | nn0z 11277 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℤ) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑖 ∈
ℤ) |
33 | 20 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
34 | 32, 33 | zaddcld 11362 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑖 + 𝑁) ∈ ℤ) |
35 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → (#‘𝑊)
∈ ℕ) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) →
(#‘𝑊) ∈
ℕ) |
37 | 34, 36 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈
ℕ)) |
38 | 37 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → ((𝑊 ∈
Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈
ℕ))) |
39 | 38 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝑖 <
(#‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈
ℕ))) |
40 | 30, 39 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈
ℕ))) |
41 | 40 | impcom 445 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈
ℕ)) |
42 | | zmodfzo 12555 |
. . . . . . . . . 10
⊢ (((𝑖 + 𝑁) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) |
44 | 2 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) = ((𝑖 + 𝑁) mod (#‘𝑊))) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) ∈ (0..^(#‘𝑊)) ↔ ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))) |
46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) ∈ (0..^(#‘𝑊)) ↔ ((𝑖 + 𝑁) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))) |
47 | 43, 46 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) ∈ (0..^(#‘𝑊))) |
48 | | cshwidxmod 13400 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀)))) = (𝑊‘((((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (#‘𝑊)))) |
49 | 28, 29, 47, 48 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀)))) = (𝑊‘((((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (#‘𝑊)))) |
50 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑖 ∈
ℝ) |
52 | | zre 11258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
53 | 52 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑁 ∈
ℝ) |
54 | 51, 53 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → (𝑖 + 𝑁) ∈
ℝ) |
55 | | zre 11258 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
56 | 55 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑀 ∈
ℝ) |
57 | | nnrp 11718 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ+) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → (#‘𝑊)
∈ ℝ+) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → (#‘𝑊) ∈
ℝ+) |
60 | | modaddmod 12571 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 + 𝑁) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ+)
→ ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = (((𝑖 + 𝑁) + 𝑀) mod (#‘𝑊))) |
61 | 54, 56, 59, 60 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → ((((𝑖 +
𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = (((𝑖 + 𝑁) + 𝑀) mod (#‘𝑊))) |
62 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℂ) |
63 | 62 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑖 ∈
ℂ) |
64 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
65 | 64 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑀 ∈
ℂ) |
66 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
67 | 66 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → 𝑁 ∈
ℂ) |
68 | | add32r 10134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑖 + (𝑀 + 𝑁)) = ((𝑖 + 𝑁) + 𝑀)) |
69 | 63, 65, 67, 68 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → (𝑖 +
(𝑀 + 𝑁)) = ((𝑖 + 𝑁) + 𝑀)) |
70 | 69 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → ((𝑖 +
𝑁) + 𝑀) = (𝑖 + (𝑀 + 𝑁))) |
71 | 70 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → (((𝑖 +
𝑁) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊))) |
72 | 61, 71 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ (𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ)) → ((((𝑖 +
𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊))) |
73 | 72 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → ((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → ((((𝑖 +
𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
74 | 73 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝑖 <
(#‘𝑊)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
75 | 30, 74 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
76 | 75 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝑊)) → ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
77 | 76 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝑊)) → ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
78 | 77 | imp 444 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊))) |
79 | 78 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊))) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
80 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (#‘(𝑊 cyclShift 𝑀)) = (#‘𝑊)) |
81 | 80 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) = ((𝑖 + 𝑁) mod (#‘𝑊))) |
82 | 81 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) = (((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀)) |
83 | 82 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (#‘𝑊)) = ((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊))) |
84 | 83 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (#‘𝑊))) = (𝑊‘((((𝑖 + 𝑁) mod (#‘𝑊)) + 𝑀) mod (#‘𝑊)))) |
85 | 10 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑀 + 𝑁) ∈ ℤ) |
86 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘𝑊))) |
87 | | cshwidxmod 13400 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
88 | 28, 85, 86, 87 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (#‘𝑊)))) |
89 | 79, 84, 88 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (#‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (#‘𝑊))) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
90 | 27, 49, 89 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
91 | 90 | ex 449 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝑊)) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖))) |
92 | 17, 91 | sylbid 229 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖))) |
93 | 92 | ralrimiv 2948 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
94 | 14, 93 | jca 553 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖))) |
95 | | cshwcl 13395 |
. . . . . 6
⊢ ((𝑊 cyclShift 𝑀) ∈ Word 𝑉 → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉) |
96 | 3, 95 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉) |
97 | | cshwcl 13395 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉) |
98 | 96, 97 | jca 553 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉 ∧ (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉)) |
99 | 98 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉 ∧ (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉)) |
100 | | eqwrd 13201 |
. . 3
⊢ ((((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉 ∧ (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)) ↔ ((#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)))) |
101 | 99, 100 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)) ↔ ((#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (#‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(#‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)))) |
102 | 94, 101 | mpbird 246 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁))) |