Metamath Proof Explorer

Theorem 2cshw

Description: Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018) (Revised by AV, 4-Jun-2018) (Revised by AV, 31-Oct-2018)

Ref Expression
Assertion 2cshw ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 cshwlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
2 1 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
3 cshwcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 )
4 cshwlen ⊢ ( ( ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) )
5 3 4 sylan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) )
6 5 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) )
7 simp1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑊 ∈ Word 𝑉 )
8 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
9 8 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
10 cshwlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) = ( ♯ ‘ 𝑊 ) )
11 7 9 10 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) = ( ♯ ‘ 𝑊 ) )
12 2 6 11 3eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) )
13 6 2 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
14 13 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 14 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
16 3 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 )
17 16 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 )
18 simpl3 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
19 2 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 19 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
21 20 biimpar ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) )
22 cshwidxmod ⊢ ( ( ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift 𝑀 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ) )
23 17 18 21 22 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift 𝑀 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ) )
24 simpl1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
25 simpl2 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑀 ∈ ℤ )
26 elfzo0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝑊 ) ) )
27 nn0z ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℤ )
28 27 ad2antrr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑖 ∈ ℤ )
29 simpr3 ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
30 28 29 zaddcld ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑖 + 𝑁 ) ∈ ℤ )
31 simplr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
32 30 31 jca ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
33 32 ex ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
34 33 3adant3 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
35 26 34 sylbi ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) )
36 35 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
37 zmodfzo ⊢ ( ( ( 𝑖 + 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 36 37 syl ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 1 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) = ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
40 39 eleq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
41 40 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
42 41 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
43 38 42 mpbird ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
44 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑀 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) )
45 24 25 43 44 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑀 ) ‘ ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) )
46 nn0re ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ )
47 46 ad2antrr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑖 ∈ ℝ )
48 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
49 48 ad2antll ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℝ )
50 47 49 readdcld ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑖 + 𝑁 ) ∈ ℝ )
51 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
52 51 ad2antrl ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℝ )
53 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
54 53 ad2antlr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
55 modaddmod ⊢ ( ( ( 𝑖 + 𝑁 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝑖 + 𝑁 ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) )
56 50 52 54 55 syl3anc ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝑖 + 𝑁 ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) )
57 nn0cn ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℂ )
58 57 ad2antrr ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑖 ∈ ℂ )
59 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
60 59 ad2antrl ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑀 ∈ ℂ )
61 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
62 61 ad2antll ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
63 add32r ⊢ ( ( 𝑖 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑖 + ( 𝑀 + 𝑁 ) ) = ( ( 𝑖 + 𝑁 ) + 𝑀 ) )
64 58 60 62 63 syl3anc ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑖 + ( 𝑀 + 𝑁 ) ) = ( ( 𝑖 + 𝑁 ) + 𝑀 ) )
65 64 oveq1d ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( ( ( 𝑖 + 𝑁 ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) )
66 56 65 eqtr4d ⊢ ( ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) )
67 66 ex ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
68 67 3adant3 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
69 26 68 sylbi ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
70 69 impcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) )
71 70 3adantl1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) = ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) )
72 71 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
73 2 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) = ( ♯ ‘ 𝑊 ) )
74 73 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) = ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
75 74 oveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) + 𝑀 ) = ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) )
76 75 fvoveq1d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) )
77 9 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
78 simpr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
79 cshwidxmod ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
80 24 77 78 79 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) = ( 𝑊 ‘ ( ( 𝑖 + ( 𝑀 + 𝑁 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
81 72 76 80 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ( 𝑖 + 𝑁 ) mod ( ♯ ‘ ( 𝑊 cyclShift 𝑀 ) ) ) + 𝑀 ) mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) )
82 23 45 81 3eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) )
83 82 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) ) )
84 15 83 sylbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) ) )
85 84 ralrimiv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) )
86 cshwcl ⊢ ( ( 𝑊 cyclShift 𝑀 ) ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ∈ Word 𝑉 )
87 3 86 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ∈ Word 𝑉 )
88 cshwcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ∈ Word 𝑉 )
89 eqwrd ⊢ ( ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ∈ Word 𝑉 ∧ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ∈ Word 𝑉 ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ↔ ( ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) ) ) )
90 87 88 89 syl2anc ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ↔ ( ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) ) ) )
91 90 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ↔ ( ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) = ( ♯ ‘ ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ) ) ( ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) ‘ 𝑖 ) = ( ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) ‘ 𝑖 ) ) ) )
92 12 85 91 mpbir2and ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑀 ) cyclShift 𝑁 ) = ( 𝑊 cyclShift ( 𝑀 + 𝑁 ) ) )