Step | Hyp | Ref
| Expression |
1 | | cshwlen 14250 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑀)) = (♯‘𝑊)) |
2 | 1 | 3adant3 1133 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
𝑀)) = (♯‘𝑊)) |
3 | | cshwcl 14249 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
4 | | cshwlen 14250 |
. . . . 5
⊢ (((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)) = (♯‘(𝑊 cyclShift 𝑀))) |
5 | 3, 4 | sylan 583 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) →
(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)) = (♯‘(𝑊 cyclShift 𝑀))) |
6 | 5 | 3adant2 1132 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)) = (♯‘(𝑊 cyclShift 𝑀))) |
7 | | simp1 1137 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑊 ∈ Word 𝑉) |
8 | | zaddcl 12103 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
9 | 8 | 3adant1 1131 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
10 | | cshwlen 14250 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝑁) ∈ ℤ) →
(♯‘(𝑊 cyclShift
(𝑀 + 𝑁))) = (♯‘𝑊)) |
11 | 7, 9, 10 | syl2anc 587 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(♯‘(𝑊 cyclShift
(𝑀 + 𝑁))) = (♯‘𝑊)) |
12 | 2, 6, 11 | 3eqtr4d 2783 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)) = (♯‘(𝑊 cyclShift (𝑀 + 𝑁)))) |
13 | 6, 2 | eqtrd 2773 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)) = (♯‘𝑊)) |
14 | 13 | oveq2d 7186 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(0..^(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁))) =
(0..^(♯‘𝑊))) |
15 | 14 | eleq2d 2818 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁))) ↔ 𝑖 ∈ (0..^(♯‘𝑊)))) |
16 | 3 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
17 | 16 | adantr 484 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊 cyclShift 𝑀) ∈ Word 𝑉) |
18 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℤ) |
19 | 2 | oveq2d 7186 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(0..^(♯‘(𝑊
cyclShift 𝑀))) =
(0..^(♯‘𝑊))) |
20 | 19 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘(𝑊 cyclShift 𝑀))) ↔ 𝑖 ∈ (0..^(♯‘𝑊)))) |
21 | 20 | biimpar 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑖 ∈ (0..^(♯‘(𝑊 cyclShift 𝑀)))) |
22 | | cshwidxmod 14254 |
. . . . . . 7
⊢ (((𝑊 cyclShift 𝑀) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ (0..^(♯‘(𝑊 cyclShift 𝑀)))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))))) |
23 | 17, 18, 21, 22 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))))) |
24 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
25 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑀 ∈ ℤ) |
26 | | elfzo0 13169 |
. . . . . . . . . . 11
⊢ (𝑖 ∈
(0..^(♯‘𝑊))
↔ (𝑖 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝑖 < (♯‘𝑊))) |
27 | | nn0z 12086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℤ) |
28 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑖 ∈
ℤ) |
29 | | simpr3 1197 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
30 | 28, 29 | zaddcld 12172 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑖 + 𝑁) ∈ ℤ) |
31 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) →
(♯‘𝑊) ∈
ℕ) |
32 | 30, 31 | jca 515 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
33 | 32 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((𝑊
∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
34 | 33 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝑖 <
(♯‘𝑊)) →
((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
35 | 26, 34 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑖 ∈
(0..^(♯‘𝑊))
→ ((𝑊 ∈ Word
𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
36 | 35 | impcom 411 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
37 | | zmodfzo 13353 |
. . . . . . . . 9
⊢ (((𝑖 + 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((𝑖 + 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑖 + 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) |
39 | 1 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ) → ((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) = ((𝑖 + 𝑁) mod (♯‘𝑊))) |
40 | 39 | eleq1d 2817 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ) → (((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) ∈ (0..^(♯‘𝑊)) ↔ ((𝑖 + 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊)))) |
41 | 40 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) ∈ (0..^(♯‘𝑊)) ↔ ((𝑖 + 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊)))) |
42 | 41 | adantr 484 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) ∈ (0..^(♯‘𝑊)) ↔ ((𝑖 + 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊)))) |
43 | 38, 42 | mpbird 260 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) ∈ (0..^(♯‘𝑊))) |
44 | | cshwidxmod 14254 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀)))) = (𝑊‘((((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (♯‘𝑊)))) |
45 | 24, 25, 43, 44 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑀)‘((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀)))) = (𝑊‘((((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (♯‘𝑊)))) |
46 | | nn0re 11985 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
47 | 46 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑖
∈ ℝ) |
48 | | zre 12066 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
49 | 48 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑁
∈ ℝ) |
50 | 47, 49 | readdcld 10748 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → (𝑖
+ 𝑁) ∈
ℝ) |
51 | | zre 12066 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
52 | 51 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑀
∈ ℝ) |
53 | | nnrp 12483 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) |
54 | 53 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → (♯‘𝑊) ∈
ℝ+) |
55 | | modaddmod 13369 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 + 𝑁) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+)
→ ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = (((𝑖 + 𝑁) + 𝑀) mod (♯‘𝑊))) |
56 | 50, 52, 54, 55 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = (((𝑖 + 𝑁) + 𝑀) mod (♯‘𝑊))) |
57 | | nn0cn 11986 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℂ) |
58 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑖
∈ ℂ) |
59 | | zcn 12067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
60 | 59 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑀
∈ ℂ) |
61 | | zcn 12067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
62 | 61 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → 𝑁
∈ ℂ) |
63 | | add32r 10937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑖 + (𝑀 + 𝑁)) = ((𝑖 + 𝑁) + 𝑀)) |
64 | 58, 60, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → (𝑖
+ (𝑀 + 𝑁)) = ((𝑖 + 𝑁) + 𝑀)) |
65 | 64 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → ((𝑖
+ (𝑀 + 𝑁)) mod (♯‘𝑊)) = (((𝑖 + 𝑁) + 𝑀) mod (♯‘𝑊))) |
66 | 56, 65 | eqtr4d 2776 |
. . . . . . . . . . . . 13
⊢ (((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝑀
∈ ℤ ∧ 𝑁
∈ ℤ)) → ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊))) |
67 | 66 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((𝑀
∈ ℤ ∧ 𝑁
∈ ℤ) → ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
68 | 67 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝑖 <
(♯‘𝑊)) →
((𝑀 ∈ ℤ ∧
𝑁 ∈ ℤ) →
((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
69 | 26, 68 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑖 ∈
(0..^(♯‘𝑊))
→ ((𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ)
→ ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
70 | 69 | impcom 411 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈
(0..^(♯‘𝑊)))
→ ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊))) |
71 | 70 | 3adantl1 1167 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)) = ((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊))) |
72 | 71 | fveq2d 6678 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊))) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
73 | 2 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (♯‘(𝑊 cyclShift 𝑀)) = (♯‘𝑊)) |
74 | 73 | oveq2d 7186 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) = ((𝑖 + 𝑁) mod (♯‘𝑊))) |
75 | 74 | oveq1d 7185 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) + 𝑀) = (((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀)) |
76 | 75 | fvoveq1d 7192 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (♯‘𝑊))) = (𝑊‘((((𝑖 + 𝑁) mod (♯‘𝑊)) + 𝑀) mod (♯‘𝑊)))) |
77 | 9 | adantr 484 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑀 + 𝑁) ∈ ℤ) |
78 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑖 ∈ (0..^(♯‘𝑊))) |
79 | | cshwidxmod 14254 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
80 | 24, 77, 78, 79 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖) = (𝑊‘((𝑖 + (𝑀 + 𝑁)) mod (♯‘𝑊)))) |
81 | 72, 76, 80 | 3eqtr4d 2783 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘((((𝑖 + 𝑁) mod (♯‘(𝑊 cyclShift 𝑀))) + 𝑀) mod (♯‘𝑊))) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
82 | 23, 45, 81 | 3eqtrd 2777 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
83 | 82 | ex 416 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘𝑊)) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖))) |
84 | 15, 83 | sylbid 243 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0..^(♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁))) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖))) |
85 | 84 | ralrimiv 3095 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∀𝑖 ∈
(0..^(♯‘((𝑊
cyclShift 𝑀) cyclShift
𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)) |
86 | | cshwcl 14249 |
. . . . 5
⊢ ((𝑊 cyclShift 𝑀) ∈ Word 𝑉 → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉) |
87 | 3, 86 | syl 17 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉) |
88 | | cshwcl 14249 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉) |
89 | | eqwrd 13998 |
. . . 4
⊢ ((((𝑊 cyclShift 𝑀) cyclShift 𝑁) ∈ Word 𝑉 ∧ (𝑊 cyclShift (𝑀 + 𝑁)) ∈ Word 𝑉) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)) ↔ ((♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (♯‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)))) |
90 | 87, 88, 89 | syl2anc 587 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)) ↔ ((♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (♯‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)))) |
91 | 90 | 3ad2ant1 1134 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)) ↔ ((♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)) = (♯‘(𝑊 cyclShift (𝑀 + 𝑁))) ∧ ∀𝑖 ∈ (0..^(♯‘((𝑊 cyclShift 𝑀) cyclShift 𝑁)))(((𝑊 cyclShift 𝑀) cyclShift 𝑁)‘𝑖) = ((𝑊 cyclShift (𝑀 + 𝑁))‘𝑖)))) |
92 | 12, 85, 91 | mpbir2and 713 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁))) |