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 WWordVLWcyclShiftL=WI0..^Wj0WI=WI+jLmodW

Proof

Step Hyp Ref Expression
1 oveq1 x=0xL=0L
2 1 oveq2d x=0I+xL=I+0L
3 2 fvoveq1d x=0WI+xLmodW=WI+0LmodW
4 3 eqeq2d x=0WI=WI+xLmodWWI=WI+0LmodW
5 4 imbi2d x=0WWordVLWcyclShiftL=WI0..^WWI=WI+xLmodWWWordVLWcyclShiftL=WI0..^WWI=WI+0LmodW
6 oveq1 x=yxL=yL
7 6 oveq2d x=yI+xL=I+yL
8 7 fvoveq1d x=yWI+xLmodW=WI+yLmodW
9 8 eqeq2d x=yWI=WI+xLmodWWI=WI+yLmodW
10 9 imbi2d x=yWWordVLWcyclShiftL=WI0..^WWI=WI+xLmodWWWordVLWcyclShiftL=WI0..^WWI=WI+yLmodW
11 oveq1 x=y+1xL=y+1L
12 11 oveq2d x=y+1I+xL=I+y+1L
13 12 fvoveq1d x=y+1WI+xLmodW=WI+y+1LmodW
14 13 eqeq2d x=y+1WI=WI+xLmodWWI=WI+y+1LmodW
15 14 imbi2d x=y+1WWordVLWcyclShiftL=WI0..^WWI=WI+xLmodWWWordVLWcyclShiftL=WI0..^WWI=WI+y+1LmodW
16 oveq1 x=jxL=jL
17 16 oveq2d x=jI+xL=I+jL
18 17 fvoveq1d x=jWI+xLmodW=WI+jLmodW
19 18 eqeq2d x=jWI=WI+xLmodWWI=WI+jLmodW
20 19 imbi2d x=jWWordVLWcyclShiftL=WI0..^WWI=WI+xLmodWWWordVLWcyclShiftL=WI0..^WWI=WI+jLmodW
21 zcn LL
22 21 mul02d L0L=0
23 22 adantl WWordVL0L=0
24 23 adantr WWordVLWcyclShiftL=WI0..^W0L=0
25 24 oveq2d WWordVLWcyclShiftL=WI0..^WI+0L=I+0
26 elfzoelz I0..^WI
27 26 zcnd I0..^WI
28 27 addid1d I0..^WI+0=I
29 28 ad2antll WWordVLWcyclShiftL=WI0..^WI+0=I
30 25 29 eqtrd WWordVLWcyclShiftL=WI0..^WI+0L=I
31 30 oveq1d WWordVLWcyclShiftL=WI0..^WI+0LmodW=ImodW
32 zmodidfzoimp I0..^WImodW=I
33 32 ad2antll WWordVLWcyclShiftL=WI0..^WImodW=I
34 31 33 eqtr2d WWordVLWcyclShiftL=WI0..^WI=I+0LmodW
35 34 fveq2d WWordVLWcyclShiftL=WI0..^WWI=WI+0LmodW
36 fveq1 W=WcyclShiftLWI+yLmodW=WcyclShiftLI+yLmodW
37 36 eqcoms WcyclShiftL=WWI+yLmodW=WcyclShiftLI+yLmodW
38 37 ad2antrl WWordVLWcyclShiftL=WI0..^WWI+yLmodW=WcyclShiftLI+yLmodW
39 38 adantl y0WWordVLWcyclShiftL=WI0..^WWI+yLmodW=WcyclShiftLI+yLmodW
40 simprll y0WWordVLWcyclShiftL=WI0..^WWWordV
41 simprlr y0WWordVLWcyclShiftL=WI0..^WL
42 elfzo0 I0..^WI0WI<W
43 nn0z I0I
44 43 adantr I0WI
45 nn0z y0y
46 zmulcl yLyL
47 45 46 sylan y0LyL
48 47 ancoms Ly0yL
49 zaddcl IyLI+yL
50 44 48 49 syl2an I0WLy0I+yL
51 simplr I0WLy0W
52 50 51 jca I0WLy0I+yLW
53 52 ex I0WLy0I+yLW
54 53 3adant3 I0WI<WLy0I+yLW
55 42 54 sylbi I0..^WLy0I+yLW
56 55 adantl WcyclShiftL=WI0..^WLy0I+yLW
57 56 expd WcyclShiftL=WI0..^WLy0I+yLW
58 57 com12 LWcyclShiftL=WI0..^Wy0I+yLW
59 58 adantl WWordVLWcyclShiftL=WI0..^Wy0I+yLW
60 59 imp WWordVLWcyclShiftL=WI0..^Wy0I+yLW
61 60 impcom y0WWordVLWcyclShiftL=WI0..^WI+yLW
62 zmodfzo I+yLWI+yLmodW0..^W
63 61 62 syl y0WWordVLWcyclShiftL=WI0..^WI+yLmodW0..^W
64 cshwidxmod WWordVLI+yLmodW0..^WWcyclShiftLI+yLmodW=WI+yLmodW+LmodW
65 40 41 63 64 syl3anc y0WWordVLWcyclShiftL=WI0..^WWcyclShiftLI+yLmodW=WI+yLmodW+LmodW
66 nn0re I0I
67 zre LL
68 nn0re y0y
69 nnrp WW+
70 remulcl yLyL
71 70 ancoms LyyL
72 readdcl IyLI+yL
73 71 72 sylan2 ILyI+yL
74 73 ancoms LyII+yL
75 74 adantl W+LyII+yL
76 simprll W+LyIL
77 simpl W+LyIW+
78 modaddmod I+yLLW+I+yLmodW+LmodW=I+yL+LmodW
79 75 76 77 78 syl3anc W+LyII+yLmodW+LmodW=I+yL+LmodW
80 recn II
81 80 adantl LyII
82 70 recnd yLyL
83 82 ancoms LyyL
84 83 adantr LyIyL
85 recn LL
86 85 adantr LyL
87 86 adantr LyIL
88 81 84 87 addassd LyII+yL+L=I+yL+L
89 recn yy
90 89 adantl Lyy
91 1cnd Ly1
92 90 91 86 adddird Lyy+1L=yL+1L
93 85 mulid2d L1L=L
94 93 adantr Ly1L=L
95 94 oveq2d LyyL+1L=yL+L
96 92 95 eqtr2d LyyL+L=y+1L
97 96 adantr LyIyL+L=y+1L
98 97 oveq2d LyII+yL+L=I+y+1L
99 88 98 eqtrd LyII+yL+L=I+y+1L
100 99 adantl W+LyII+yL+L=I+y+1L
101 100 oveq1d W+LyII+yL+LmodW=I+y+1LmodW
102 79 101 eqtrd W+LyII+yLmodW+LmodW=I+y+1LmodW
103 102 ex W+LyII+yLmodW+LmodW=I+y+1LmodW
104 69 103 syl WLyII+yLmodW+LmodW=I+y+1LmodW
105 104 expd WLyII+yLmodW+LmodW=I+y+1LmodW
106 105 com12 LyWII+yLmodW+LmodW=I+y+1LmodW
107 67 68 106 syl2an Ly0WII+yLmodW+LmodW=I+y+1LmodW
108 107 com13 IWLy0I+yLmodW+LmodW=I+y+1LmodW
109 66 108 syl I0WLy0I+yLmodW+LmodW=I+y+1LmodW
110 109 imp I0WLy0I+yLmodW+LmodW=I+y+1LmodW
111 110 3adant3 I0WI<WLy0I+yLmodW+LmodW=I+y+1LmodW
112 42 111 sylbi I0..^WLy0I+yLmodW+LmodW=I+y+1LmodW
113 112 expd I0..^WLy0I+yLmodW+LmodW=I+y+1LmodW
114 113 adantld I0..^WWWordVLy0I+yLmodW+LmodW=I+y+1LmodW
115 114 adantl WcyclShiftL=WI0..^WWWordVLy0I+yLmodW+LmodW=I+y+1LmodW
116 115 impcom WWordVLWcyclShiftL=WI0..^Wy0I+yLmodW+LmodW=I+y+1LmodW
117 116 impcom y0WWordVLWcyclShiftL=WI0..^WI+yLmodW+LmodW=I+y+1LmodW
118 117 fveq2d y0WWordVLWcyclShiftL=WI0..^WWI+yLmodW+LmodW=WI+y+1LmodW
119 39 65 118 3eqtrd y0WWordVLWcyclShiftL=WI0..^WWI+yLmodW=WI+y+1LmodW
120 119 eqeq2d y0WWordVLWcyclShiftL=WI0..^WWI=WI+yLmodWWI=WI+y+1LmodW
121 120 biimpd y0WWordVLWcyclShiftL=WI0..^WWI=WI+yLmodWWI=WI+y+1LmodW
122 121 ex y0WWordVLWcyclShiftL=WI0..^WWI=WI+yLmodWWI=WI+y+1LmodW
123 122 a2d y0WWordVLWcyclShiftL=WI0..^WWI=WI+yLmodWWWordVLWcyclShiftL=WI0..^WWI=WI+y+1LmodW
124 5 10 15 20 35 123 nn0ind j0WWordVLWcyclShiftL=WI0..^WWI=WI+jLmodW
125 124 com12 WWordVLWcyclShiftL=WI0..^Wj0WI=WI+jLmodW
126 125 ralrimiv WWordVLWcyclShiftL=WI0..^Wj0WI=WI+jLmodW
127 126 ex WWordVLWcyclShiftL=WI0..^Wj0WI=WI+jLmodW