Metamath Proof Explorer

Theorem cshwshash

Description: If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by AV, 19-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 
|- M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
Assertion cshwshash 
|- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 
 |-  M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
2 repswsymballbi 
 |-  ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
3 2 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
4 prmnn 
 |-  ( ( # ` W ) e. Prime -> ( # ` W ) e. NN )
5 4 nnge1d 
 |-  ( ( # ` W ) e. Prime -> 1 <_ ( # ` W ) )
6 wrdsymb1 
 |-  ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )
7 5 6 sylan2 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( W ` 0 ) e. V )
8 7 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( W ` 0 ) e. V )
9 4 ad2antlr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( # ` W ) e. NN )
10 simpr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )
11 1 cshwrepswhash1 
 |-  ( ( ( W ` 0 ) e. V /\ ( # ` W ) e. NN /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( # ` M ) = 1 )
12 8 9 10 11 syl3anc 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) -> ( # ` M ) = 1 )
13 12 ex 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) -> ( # ` M ) = 1 ) )
14 3 13 sylbird 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( # ` M ) = 1 ) )
15 olc 
 |-  ( ( # ` M ) = 1 -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) )
16 14 15 syl6com 
 |-  ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) ) )
17 rexnal 
 |-  ( E. i e. ( 0 ..^ ( # ` W ) ) -. ( W ` i ) = ( W ` 0 ) <-> -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
18 df-ne 
 |-  ( ( W ` i ) =/= ( W ` 0 ) <-> -. ( W ` i ) = ( W ` 0 ) )
19 18 bicomi 
 |-  ( -. ( W ` i ) = ( W ` 0 ) <-> ( W ` i ) =/= ( W ` 0 ) )
20 19 rexbii 
 |-  ( E. i e. ( 0 ..^ ( # ` W ) ) -. ( W ` i ) = ( W ` 0 ) <-> E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) )
21 17 20 bitr3i 
 |-  ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) )
22 1 cshwshashnsame 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( # ` M ) = ( # ` W ) ) )
23 orc 
 |-  ( ( # ` M ) = ( # ` W ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) )
24 22 23 syl6com 
 |-  ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) ) )
25 21 24 sylbi 
 |-  ( -. A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) -> ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) ) )
26 16 25 pm2.61i 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) )