# 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 ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({W}\mathrm{cyclShift}{M}\right)\mathrm{cyclShift}{N}={W}\mathrm{cyclShift}\left({M}+{N}\right)$

### Proof

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