Metamath Proof Explorer

Theorem cshwshashnsame

Description: If a word (not consisting of identical symbols) 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. (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 cshwshashnsame 
|- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( # ` M ) = ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 
 |-  M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
2 1 cshwsiun 
 |-  ( W e. Word V -> M = U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )
3 2 ad2antrr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> M = U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )
4 3 fveq2d 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( # ` M ) = ( # ` U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } ) )
5 fzofi 
 |-  ( 0 ..^ ( # ` W ) ) e. Fin
6 5 a1i 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( 0 ..^ ( # ` W ) ) e. Fin )
7 snfi 
 |-  { ( W cyclShift n ) } e. Fin
8 7 a1i 
 |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> { ( W cyclShift n ) } e. Fin )
9 id 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( W e. Word V /\ ( # ` W ) e. Prime ) )
10 9 cshwsdisj 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> Disj_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )
11 6 8 10 hashiun 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( # ` U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } ) = sum_ n e. ( 0 ..^ ( # ` W ) ) ( # ` { ( W cyclShift n ) } ) )
12 ovex 
 |-  ( W cyclShift n ) e. _V
13 hashsng 
 |-  ( ( W cyclShift n ) e. _V -> ( # ` { ( W cyclShift n ) } ) = 1 )
14 12 13 mp1i 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( # ` { ( W cyclShift n ) } ) = 1 )
15 14 sumeq2sdv 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) ( # ` { ( W cyclShift n ) } ) = sum_ n e. ( 0 ..^ ( # ` W ) ) 1 )
16 1cnd 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> 1 e. CC )
17 fsumconst 
 |-  ( ( ( 0 ..^ ( # ` W ) ) e. Fin /\ 1 e. CC ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) 1 = ( ( # ` ( 0 ..^ ( # ` W ) ) ) x. 1 ) )
18 5 16 17 sylancr 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) 1 = ( ( # ` ( 0 ..^ ( # ` W ) ) ) x. 1 ) )
19 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
20 19 adantr 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` W ) e. NN0 )
21 hashfzo0 
 |-  ( ( # ` W ) e. NN0 -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
22 20 21 syl 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
23 22 oveq1d 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` ( 0 ..^ ( # ` W ) ) ) x. 1 ) = ( ( # ` W ) x. 1 ) )
24 prmnn 
 |-  ( ( # ` W ) e. Prime -> ( # ` W ) e. NN )
25 24 nnred 
 |-  ( ( # ` W ) e. Prime -> ( # ` W ) e. RR )
26 25 adantl 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` W ) e. RR )
27 ax-1rid 
 |-  ( ( # ` W ) e. RR -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
28 26 27 syl 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` W ) x. 1 ) = ( # ` W ) )
29 18 23 28 3eqtrd 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) 1 = ( # ` W ) )
30 29 adantr 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) 1 = ( # ` W ) )
31 15 30 eqtrd 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> sum_ n e. ( 0 ..^ ( # ` W ) ) ( # ` { ( W cyclShift n ) } ) = ( # ` W ) )
32 4 11 31 3eqtrd 
 |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( # ` M ) = ( # ` W ) )
33 32 ex 
 |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( E. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( # ` M ) = ( # ` W ) ) )