Metamath Proof Explorer

Theorem cshwrepswhash1

Description: The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018) (Revised by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 
|- M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
Assertion cshwrepswhash1 
|- ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> ( # ` 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 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 repsdf2 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( W = ( A repeatS N ) <-> ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) )
4 2 3 sylan2 
 |-  ( ( A e. V /\ N e. NN ) -> ( W = ( A repeatS N ) <-> ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) )
5 simp1 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> W e. Word V )
6 5 adantl 
 |-  ( ( ( A e. V /\ N e. NN ) /\ ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) -> W e. Word V )
7 eleq1 
 |-  ( N = ( # ` W ) -> ( N e. NN <-> ( # ` W ) e. NN ) )
8 7 eqcoms 
 |-  ( ( # ` W ) = N -> ( N e. NN <-> ( # ` W ) e. NN ) )
9 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
10 9 biimpri 
 |-  ( ( # ` W ) e. NN -> 0 e. ( 0 ..^ ( # ` W ) ) )
11 8 10 syl6bi 
 |-  ( ( # ` W ) = N -> ( N e. NN -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
12 11 3ad2ant2 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> ( N e. NN -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
13 12 com12 
 |-  ( N e. NN -> ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
14 13 adantl 
 |-  ( ( A e. V /\ N e. NN ) -> ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> 0 e. ( 0 ..^ ( # ` W ) ) ) )
15 14 imp 
 |-  ( ( ( A e. V /\ N e. NN ) /\ ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
16 cshw0 
 |-  ( W e. Word V -> ( W cyclShift 0 ) = W )
17 6 16 syl 
 |-  ( ( ( A e. V /\ N e. NN ) /\ ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) -> ( W cyclShift 0 ) = W )
18 oveq2 
 |-  ( n = 0 -> ( W cyclShift n ) = ( W cyclShift 0 ) )
19 18 eqeq1d 
 |-  ( n = 0 -> ( ( W cyclShift n ) = W <-> ( W cyclShift 0 ) = W ) )
20 19 rspcev 
 |-  ( ( 0 e. ( 0 ..^ ( # ` W ) ) /\ ( W cyclShift 0 ) = W ) -> E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = W )
21 15 17 20 syl2anc 
 |-  ( ( ( A e. V /\ N e. NN ) /\ ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) -> E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = W )
22 eqeq2 
 |-  ( w = W -> ( ( W cyclShift n ) = w <-> ( W cyclShift n ) = W ) )
23 22 rexbidv 
 |-  ( w = W -> ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = W ) )
24 23 rspcev 
 |-  ( ( W e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = W ) -> E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w )
25 6 21 24 syl2anc 
 |-  ( ( ( A e. V /\ N e. NN ) /\ ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) ) -> E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w )
26 25 ex 
 |-  ( ( A e. V /\ N e. NN ) -> ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) )
27 4 26 sylbid 
 |-  ( ( A e. V /\ N e. NN ) -> ( W = ( A repeatS N ) -> E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) )
28 27 3impia 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w )
29 repsw 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( A repeatS N ) e. Word V )
30 2 29 sylan2 
 |-  ( ( A e. V /\ N e. NN ) -> ( A repeatS N ) e. Word V )
31 30 3adant3 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> ( A repeatS N ) e. Word V )
32 simpll3 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> W = ( A repeatS N ) )
33 32 oveq1d 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift n ) = ( ( A repeatS N ) cyclShift n ) )
34 simp1 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> A e. V )
35 34 ad2antrr 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> A e. V )
36 2 3ad2ant2 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> N e. NN0 )
37 36 ad2antrr 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> N e. NN0 )
38 elfzoelz 
 |-  ( n e. ( 0 ..^ ( # ` W ) ) -> n e. ZZ )
39 38 adantl 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> n e. ZZ )
40 repswcshw 
 |-  ( ( A e. V /\ N e. NN0 /\ n e. ZZ ) -> ( ( A repeatS N ) cyclShift n ) = ( A repeatS N ) )
41 35 37 39 40 syl3anc 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( ( A repeatS N ) cyclShift n ) = ( A repeatS N ) )
42 33 41 eqtrd 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift n ) = ( A repeatS N ) )
43 42 eqeq1d 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift n ) = u <-> ( A repeatS N ) = u ) )
44 43 biimpd 
 |-  ( ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift n ) = u -> ( A repeatS N ) = u ) )
45 44 rexlimdva 
 |-  ( ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) /\ u e. Word V ) -> ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> ( A repeatS N ) = u ) )
46 45 ralrimiva 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> ( A repeatS N ) = u ) )
47 eqeq1 
 |-  ( w = ( A repeatS N ) -> ( w = u <-> ( A repeatS N ) = u ) )
48 47 imbi2d 
 |-  ( w = ( A repeatS N ) -> ( ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> w = u ) <-> ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> ( A repeatS N ) = u ) ) )
49 48 ralbidv 
 |-  ( w = ( A repeatS N ) -> ( A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> w = u ) <-> A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> ( A repeatS N ) = u ) ) )
50 49 rspcev 
 |-  ( ( ( A repeatS N ) e. Word V /\ A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> ( A repeatS N ) = u ) ) -> E. w e. Word V A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> w = u ) )
51 31 46 50 syl2anc 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> E. w e. Word V A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> w = u ) )
52 eqeq2 
 |-  ( w = u -> ( ( W cyclShift n ) = w <-> ( W cyclShift n ) = u ) )
53 52 rexbidv 
 |-  ( w = u -> ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u ) )
54 53 reu7 
 |-  ( E! w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> ( E. w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w /\ E. w e. Word V A. u e. Word V ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = u -> w = u ) ) )
55 28 51 54 sylanbrc 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> E! w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w )
56 reusn 
 |-  ( E! w e. Word V E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> E. r { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { r } )
57 55 56 sylib 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> E. r { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { r } )
58 1 eqeq1i 
 |-  ( M = { r } <-> { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { r } )
59 58 exbii 
 |-  ( E. r M = { r } <-> E. r { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { r } )
60 57 59 sylibr 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> E. r M = { r } )
61 1 cshwsex 
 |-  ( W e. Word V -> M e. _V )
62 61 3ad2ant1 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = A ) -> M e. _V )
63 4 62 syl6bi 
 |-  ( ( A e. V /\ N e. NN ) -> ( W = ( A repeatS N ) -> M e. _V ) )
64 63 3impia 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> M e. _V )
65 hash1snb 
 |-  ( M e. _V -> ( ( # ` M ) = 1 <-> E. r M = { r } ) )
66 64 65 syl 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> ( ( # ` M ) = 1 <-> E. r M = { r } ) )
67 60 66 mpbird 
 |-  ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> ( # ` M ) = 1 )