Metamath Proof Explorer

Theorem cshweqrep

Description: If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion cshweqrep 
|- ( ( W e. Word V /\ L e. ZZ ) -> ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> A. j e. NN0 ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = 0 -> ( x x. L ) = ( 0 x. L ) )
2 1 oveq2d 
 |-  ( x = 0 -> ( I + ( x x. L ) ) = ( I + ( 0 x. L ) ) )
3 2 fvoveq1d 
 |-  ( x = 0 -> ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) ) )
4 3 eqeq2d 
 |-  ( x = 0 -> ( ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) <-> ( W ` I ) = ( W ` ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) ) ) )
5 4 imbi2d 
 |-  ( x = 0 -> ( ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) ) <-> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) ) ) ) )
6 oveq1 
 |-  ( x = y -> ( x x. L ) = ( y x. L ) )
7 6 oveq2d 
 |-  ( x = y -> ( I + ( x x. L ) ) = ( I + ( y x. L ) ) )
8 7 fvoveq1d 
 |-  ( x = y -> ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) )
9 8 eqeq2d 
 |-  ( x = y -> ( ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) <-> ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) ) )
10 9 imbi2d 
 |-  ( x = y -> ( ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) ) <-> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) ) ) )
11 oveq1 
 |-  ( x = ( y + 1 ) -> ( x x. L ) = ( ( y + 1 ) x. L ) )
12 11 oveq2d 
 |-  ( x = ( y + 1 ) -> ( I + ( x x. L ) ) = ( I + ( ( y + 1 ) x. L ) ) )
13 12 fvoveq1d 
 |-  ( x = ( y + 1 ) -> ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
14 13 eqeq2d 
 |-  ( x = ( y + 1 ) -> ( ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) <-> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
15 14 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) ) <-> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) ) )
16 oveq1 
 |-  ( x = j -> ( x x. L ) = ( j x. L ) )
17 16 oveq2d 
 |-  ( x = j -> ( I + ( x x. L ) ) = ( I + ( j x. L ) ) )
18 17 fvoveq1d 
 |-  ( x = j -> ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) )
19 18 eqeq2d 
 |-  ( x = j -> ( ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) <-> ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) )
20 19 imbi2d 
 |-  ( x = j -> ( ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( x x. L ) ) mod ( # ` W ) ) ) ) <-> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) ) )
21 zcn 
 |-  ( L e. ZZ -> L e. CC )
22 21 mul02d 
 |-  ( L e. ZZ -> ( 0 x. L ) = 0 )
23 22 adantl 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( 0 x. L ) = 0 )
24 23 adantr 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( 0 x. L ) = 0 )
25 24 oveq2d 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I + ( 0 x. L ) ) = ( I + 0 ) )
26 elfzoelz 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ZZ )
27 26 zcnd 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. CC )
28 27 addid1d 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I + 0 ) = I )
29 28 ad2antll 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I + 0 ) = I )
30 25 29 eqtrd 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I + ( 0 x. L ) ) = I )
31 30 oveq1d 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) = ( I mod ( # ` W ) ) )
32 zmodidfzoimp 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I mod ( # ` W ) ) = I )
33 32 ad2antll 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( I mod ( # ` W ) ) = I )
34 31 33 eqtr2d 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> I = ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) )
35 34 fveq2d 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( 0 x. L ) ) mod ( # ` W ) ) ) )
36 fveq1 
 |-  ( W = ( W cyclShift L ) -> ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) )
37 36 eqcoms 
 |-  ( ( W cyclShift L ) = W -> ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) )
38 37 ad2antrl 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) )
39 38 adantl 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) )
40 simprll 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> W e. Word V )
41 simprlr 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> L e. ZZ )
42 elfzo0 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) )
43 nn0z 
 |-  ( I e. NN0 -> I e. ZZ )
44 43 adantr 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN ) -> I e. ZZ )
45 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
46 zmulcl 
 |-  ( ( y e. ZZ /\ L e. ZZ ) -> ( y x. L ) e. ZZ )
47 45 46 sylan 
 |-  ( ( y e. NN0 /\ L e. ZZ ) -> ( y x. L ) e. ZZ )
48 47 ancoms 
 |-  ( ( L e. ZZ /\ y e. NN0 ) -> ( y x. L ) e. ZZ )
49 zaddcl 
 |-  ( ( I e. ZZ /\ ( y x. L ) e. ZZ ) -> ( I + ( y x. L ) ) e. ZZ )
50 44 48 49 syl2an 
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ ( L e. ZZ /\ y e. NN0 ) ) -> ( I + ( y x. L ) ) e. ZZ )
51 simplr 
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ ( L e. ZZ /\ y e. NN0 ) ) -> ( # ` W ) e. NN )
52 50 51 jca 
 |-  ( ( ( I e. NN0 /\ ( # ` W ) e. NN ) /\ ( L e. ZZ /\ y e. NN0 ) ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) )
53 52 ex 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) )
54 53 3adant3 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) )
55 42 54 sylbi 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) )
56 55 adantl 
 |-  ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) )
57 56 expd 
 |-  ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( L e. ZZ -> ( y e. NN0 -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) ) )
58 57 com12 
 |-  ( L e. ZZ -> ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( y e. NN0 -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) ) )
59 58 adantl 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( y e. NN0 -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) ) )
60 59 imp 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( y e. NN0 -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) ) )
61 60 impcom 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) )
62 zmodfzo 
 |-  ( ( ( I + ( y x. L ) ) e. ZZ /\ ( # ` W ) e. NN ) -> ( ( I + ( y x. L ) ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
63 61 62 syl 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( I + ( y x. L ) ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) )
64 cshwidxmod 
 |-  ( ( W e. Word V /\ L e. ZZ /\ ( ( I + ( y x. L ) ) mod ( # ` W ) ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) ) )
65 40 41 63 64 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( W cyclShift L ) ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) ) )
66 nn0re 
 |-  ( I e. NN0 -> I e. RR )
67 zre 
 |-  ( L e. ZZ -> L e. RR )
68 nn0re 
 |-  ( y e. NN0 -> y e. RR )
69 nnrp 
 |-  ( ( # ` W ) e. NN -> ( # ` W ) e. RR+ )
70 remulcl 
 |-  ( ( y e. RR /\ L e. RR ) -> ( y x. L ) e. RR )
71 70 ancoms 
 |-  ( ( L e. RR /\ y e. RR ) -> ( y x. L ) e. RR )
72 readdcl 
 |-  ( ( I e. RR /\ ( y x. L ) e. RR ) -> ( I + ( y x. L ) ) e. RR )
73 71 72 sylan2 
 |-  ( ( I e. RR /\ ( L e. RR /\ y e. RR ) ) -> ( I + ( y x. L ) ) e. RR )
74 73 ancoms 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( I + ( y x. L ) ) e. RR )
75 74 adantl 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( I + ( y x. L ) ) e. RR )
76 simprll 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> L e. RR )
77 simpl 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( # ` W ) e. RR+ )
78 modaddmod 
 |-  ( ( ( I + ( y x. L ) ) e. RR /\ L e. RR /\ ( # ` W ) e. RR+ ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( ( I + ( y x. L ) ) + L ) mod ( # ` W ) ) )
79 75 76 77 78 syl3anc 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( ( I + ( y x. L ) ) + L ) mod ( # ` W ) ) )
80 recn 
 |-  ( I e. RR -> I e. CC )
81 80 adantl 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> I e. CC )
82 70 recnd 
 |-  ( ( y e. RR /\ L e. RR ) -> ( y x. L ) e. CC )
83 82 ancoms 
 |-  ( ( L e. RR /\ y e. RR ) -> ( y x. L ) e. CC )
84 83 adantr 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( y x. L ) e. CC )
85 recn 
 |-  ( L e. RR -> L e. CC )
86 85 adantr 
 |-  ( ( L e. RR /\ y e. RR ) -> L e. CC )
87 86 adantr 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> L e. CC )
88 81 84 87 addassd 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( ( I + ( y x. L ) ) + L ) = ( I + ( ( y x. L ) + L ) ) )
89 recn 
 |-  ( y e. RR -> y e. CC )
90 89 adantl 
 |-  ( ( L e. RR /\ y e. RR ) -> y e. CC )
91 1cnd 
 |-  ( ( L e. RR /\ y e. RR ) -> 1 e. CC )
92 90 91 86 adddird 
 |-  ( ( L e. RR /\ y e. RR ) -> ( ( y + 1 ) x. L ) = ( ( y x. L ) + ( 1 x. L ) ) )
93 85 mulid2d 
 |-  ( L e. RR -> ( 1 x. L ) = L )
94 93 adantr 
 |-  ( ( L e. RR /\ y e. RR ) -> ( 1 x. L ) = L )
95 94 oveq2d 
 |-  ( ( L e. RR /\ y e. RR ) -> ( ( y x. L ) + ( 1 x. L ) ) = ( ( y x. L ) + L ) )
96 92 95 eqtr2d 
 |-  ( ( L e. RR /\ y e. RR ) -> ( ( y x. L ) + L ) = ( ( y + 1 ) x. L ) )
97 96 adantr 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( ( y x. L ) + L ) = ( ( y + 1 ) x. L ) )
98 97 oveq2d 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( I + ( ( y x. L ) + L ) ) = ( I + ( ( y + 1 ) x. L ) ) )
99 88 98 eqtrd 
 |-  ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( ( I + ( y x. L ) ) + L ) = ( I + ( ( y + 1 ) x. L ) ) )
100 99 adantl 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( ( I + ( y x. L ) ) + L ) = ( I + ( ( y + 1 ) x. L ) ) )
101 100 oveq1d 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( ( ( I + ( y x. L ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) )
102 79 101 eqtrd 
 |-  ( ( ( # ` W ) e. RR+ /\ ( ( L e. RR /\ y e. RR ) /\ I e. RR ) ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) )
103 102 ex 
 |-  ( ( # ` W ) e. RR+ -> ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
104 69 103 syl 
 |-  ( ( # ` W ) e. NN -> ( ( ( L e. RR /\ y e. RR ) /\ I e. RR ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
105 104 expd 
 |-  ( ( # ` W ) e. NN -> ( ( L e. RR /\ y e. RR ) -> ( I e. RR -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
106 105 com12 
 |-  ( ( L e. RR /\ y e. RR ) -> ( ( # ` W ) e. NN -> ( I e. RR -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
107 67 68 106 syl2an 
 |-  ( ( L e. ZZ /\ y e. NN0 ) -> ( ( # ` W ) e. NN -> ( I e. RR -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
108 107 com13 
 |-  ( I e. RR -> ( ( # ` W ) e. NN -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
109 66 108 syl 
 |-  ( I e. NN0 -> ( ( # ` W ) e. NN -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
110 109 imp 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
111 110 3adant3 
 |-  ( ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
112 42 111 sylbi 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( ( L e. ZZ /\ y e. NN0 ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
113 112 expd 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( L e. ZZ -> ( y e. NN0 -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
114 113 adantld 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( ( W e. Word V /\ L e. ZZ ) -> ( y e. NN0 -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
115 114 adantl 
 |-  ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W e. Word V /\ L e. ZZ ) -> ( y e. NN0 -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
116 115 impcom 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( y e. NN0 -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
117 116 impcom 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) = ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) )
118 117 fveq2d 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W ` ( ( ( ( I + ( y x. L ) ) mod ( # ` W ) ) + L ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
119 39 65 118 3eqtrd 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) )
120 119 eqeq2d 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) <-> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
121 120 biimpd 
 |-  ( ( y e. NN0 /\ ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) ) -> ( ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) )
122 121 ex 
 |-  ( y e. NN0 -> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) ) )
123 122 a2d 
 |-  ( y e. NN0 -> ( ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( y x. L ) ) mod ( # ` W ) ) ) ) -> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( ( y + 1 ) x. L ) ) mod ( # ` W ) ) ) ) ) )
124 5 10 15 20 35 123 nn0ind 
 |-  ( j e. NN0 -> ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) )
125 124 com12 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> ( j e. NN0 -> ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) )
126 125 ralrimiv 
 |-  ( ( ( W e. Word V /\ L e. ZZ ) /\ ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) ) -> A. j e. NN0 ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) )
127 126 ex 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( ( W cyclShift L ) = W /\ I e. ( 0 ..^ ( # ` W ) ) ) -> A. j e. NN0 ( W ` I ) = ( W ` ( ( I + ( j x. L ) ) mod ( # ` W ) ) ) ) )