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 
|- ( ( W e. Word V /\ M e. ZZ /\ N e. ZZ ) -> ( ( W cyclShift M ) cyclShift N ) = ( W cyclShift ( M + N ) ) )

Proof

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