Metamath Proof Explorer

Theorem cshw1

Description: If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Proof shortened by AV, 1-Nov-2018)

Ref Expression
Assertion cshw1 
|- ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. i e. (/) ( W ` i ) = ( W ` 0 )
2 oveq2 
 |-  ( ( # ` W ) = 0 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 0 ) )
3 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
4 2 3 eqtrdi 
 |-  ( ( # ` W ) = 0 -> ( 0 ..^ ( # ` W ) ) = (/) )
5 4 raleqdv 
 |-  ( ( # ` W ) = 0 -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> A. i e. (/) ( W ` i ) = ( W ` 0 ) ) )
6 1 5 mpbiri 
 |-  ( ( # ` W ) = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
7 6 a1d 
 |-  ( ( # ` W ) = 0 -> ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
8 simprl 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> W e. Word V )
9 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
10 1nn0 
 |-  1 e. NN0
11 10 a1i 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> 1 e. NN0 )
12 df-ne 
 |-  ( ( # ` W ) =/= 0 <-> -. ( # ` W ) = 0 )
13 elnnne0 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) )
14 13 simplbi2com 
 |-  ( ( # ` W ) =/= 0 -> ( ( # ` W ) e. NN0 -> ( # ` W ) e. NN ) )
15 12 14 sylbir 
 |-  ( -. ( # ` W ) = 0 -> ( ( # ` W ) e. NN0 -> ( # ` W ) e. NN ) )
16 15 adantr 
 |-  ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> ( ( # ` W ) e. NN0 -> ( # ` W ) e. NN ) )
17 16 impcom 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> ( # ` W ) e. NN )
18 neqne 
 |-  ( -. ( # ` W ) = 1 -> ( # ` W ) =/= 1 )
19 18 ad2antll 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> ( # ` W ) =/= 1 )
20 nngt1ne1 
 |-  ( ( # ` W ) e. NN -> ( 1 < ( # ` W ) <-> ( # ` W ) =/= 1 ) )
21 17 20 syl 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> ( 1 < ( # ` W ) <-> ( # ` W ) =/= 1 ) )
22 19 21 mpbird 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> 1 < ( # ` W ) )
23 elfzo0 
 |-  ( 1 e. ( 0 ..^ ( # ` W ) ) <-> ( 1 e. NN0 /\ ( # ` W ) e. NN /\ 1 < ( # ` W ) ) )
24 11 17 22 23 syl3anbrc 
 |-  ( ( ( # ` W ) e. NN0 /\ ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) ) -> 1 e. ( 0 ..^ ( # ` W ) ) )
25 24 ex 
 |-  ( ( # ` W ) e. NN0 -> ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> 1 e. ( 0 ..^ ( # ` W ) ) ) )
26 9 25 syl 
 |-  ( W e. Word V -> ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> 1 e. ( 0 ..^ ( # ` W ) ) ) )
27 26 adantr 
 |-  ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> 1 e. ( 0 ..^ ( # ` W ) ) ) )
28 27 impcom 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> 1 e. ( 0 ..^ ( # ` W ) ) )
29 simprr 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> ( W cyclShift 1 ) = W )
30 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
31 30 13 sylbbr 
 |-  ( ( ( # ` W ) e. NN0 /\ ( # ` W ) =/= 0 ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
32 31 ex 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) =/= 0 -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
33 12 32 biimtrrid 
 |-  ( ( # ` W ) e. NN0 -> ( -. ( # ` W ) = 0 -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
34 9 33 syl 
 |-  ( W e. Word V -> ( -. ( # ` W ) = 0 -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
35 34 adantr 
 |-  ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> ( -. ( # ` W ) = 0 -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
36 35 com12 
 |-  ( -. ( # ` W ) = 0 -> ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
37 36 adantr 
 |-  ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
38 37 imp 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
39 elfzoelz 
 |-  ( 1 e. ( 0 ..^ ( # ` W ) ) -> 1 e. ZZ )
40 cshweqrep 
 |-  ( ( W e. Word V /\ 1 e. ZZ ) -> ( ( ( W cyclShift 1 ) = W /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) ) )
41 39 40 sylan2 
 |-  ( ( W e. Word V /\ 1 e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( W cyclShift 1 ) = W /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) ) )
42 41 imp 
 |-  ( ( ( W e. Word V /\ 1 e. ( 0 ..^ ( # ` W ) ) ) /\ ( ( W cyclShift 1 ) = W /\ 0 e. ( 0 ..^ ( # ` W ) ) ) ) -> A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) )
43 8 28 29 38 42 syl22anc 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) )
44 0nn0 
 |-  0 e. NN0
45 fzossnn0 
 |-  ( 0 e. NN0 -> ( 0 ..^ ( # ` W ) ) C_ NN0 )
46 ssralv 
 |-  ( ( 0 ..^ ( # ` W ) ) C_ NN0 -> ( A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) ) )
47 44 45 46 mp2b 
 |-  ( A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) )
48 eqcom 
 |-  ( ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) <-> ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )
49 elfzoelz 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> i e. ZZ )
50 zre 
 |-  ( i e. ZZ -> i e. RR )
51 ax-1rid 
 |-  ( i e. RR -> ( i x. 1 ) = i )
52 50 51 syl 
 |-  ( i e. ZZ -> ( i x. 1 ) = i )
53 52 oveq2d 
 |-  ( i e. ZZ -> ( 0 + ( i x. 1 ) ) = ( 0 + i ) )
54 zcn 
 |-  ( i e. ZZ -> i e. CC )
55 54 addlidd 
 |-  ( i e. ZZ -> ( 0 + i ) = i )
56 53 55 eqtrd 
 |-  ( i e. ZZ -> ( 0 + ( i x. 1 ) ) = i )
57 49 56 syl 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( 0 + ( i x. 1 ) ) = i )
58 57 oveq1d 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) = ( i mod ( # ` W ) ) )
59 zmodidfzoimp 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( i mod ( # ` W ) ) = i )
60 58 59 eqtrd 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) = i )
61 60 fveqeq2d 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) = ( W ` 0 ) <-> ( W ` i ) = ( W ` 0 ) ) )
62 61 biimpd 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) = ( W ` 0 ) -> ( W ` i ) = ( W ` 0 ) ) )
63 48 62 biimtrid 
 |-  ( i e. ( 0 ..^ ( # ` W ) ) -> ( ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) ) )
64 63 ralimia 
 |-  ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
65 47 64 syl 
 |-  ( A. i e. NN0 ( W ` 0 ) = ( W ` ( ( 0 + ( i x. 1 ) ) mod ( # ` W ) ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
66 43 65 syl 
 |-  ( ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
67 66 ex 
 |-  ( ( -. ( # ` W ) = 0 /\ -. ( # ` W ) = 1 ) -> ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
68 67 impancom 
 |-  ( ( -. ( # ` W ) = 0 /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> ( -. ( # ` W ) = 1 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
69 eqid 
 |-  ( W ` 0 ) = ( W ` 0 )
70 c0ex 
 |-  0 e. _V
71 fveqeq2 
 |-  ( i = 0 -> ( ( W ` i ) = ( W ` 0 ) <-> ( W ` 0 ) = ( W ` 0 ) ) )
72 70 71 ralsn 
 |-  ( A. i e. { 0 } ( W ` i ) = ( W ` 0 ) <-> ( W ` 0 ) = ( W ` 0 ) )
73 69 72 mpbir 
 |-  A. i e. { 0 } ( W ` i ) = ( W ` 0 )
74 oveq2 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 1 ) )
75 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
76 74 75 eqtrdi 
 |-  ( ( # ` W ) = 1 -> ( 0 ..^ ( # ` W ) ) = { 0 } )
77 76 raleqdv 
 |-  ( ( # ` W ) = 1 -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> A. i e. { 0 } ( W ` i ) = ( W ` 0 ) ) )
78 73 77 mpbiri 
 |-  ( ( # ` W ) = 1 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
79 68 78 pm2.61d2 
 |-  ( ( -. ( # ` W ) = 0 /\ ( W e. Word V /\ ( W cyclShift 1 ) = W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
80 79 ex 
 |-  ( -. ( # ` W ) = 0 -> ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
81 7 80 pm2.61i 
 |-  ( ( W e. Word V /\ ( W cyclShift 1 ) = W ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )