Metamath Proof Explorer

Theorem cshws0

Description: The size of the set of (different!) words resulting by cyclically shifting an empty word is 0. (Contributed 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 cshws0 
|- ( W = (/) -> ( # ` M ) = 0 )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 
 |-  M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
2 0ex 
 |-  (/) e. _V
3 eleq1 
 |-  ( W = (/) -> ( W e. _V <-> (/) e. _V ) )
4 2 3 mpbiri 
 |-  ( W = (/) -> W e. _V )
5 hasheq0 
 |-  ( W e. _V -> ( ( # ` W ) = 0 <-> W = (/) ) )
6 5 bicomd 
 |-  ( W e. _V -> ( W = (/) <-> ( # ` W ) = 0 ) )
7 4 6 syl 
 |-  ( W = (/) -> ( W = (/) <-> ( # ` W ) = 0 ) )
8 7 ibi 
 |-  ( W = (/) -> ( # ` W ) = 0 )
9 8 oveq2d 
 |-  ( W = (/) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 0 ) )
10 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
11 9 10 eqtrdi 
 |-  ( W = (/) -> ( 0 ..^ ( # ` W ) ) = (/) )
12 11 rexeqdv 
 |-  ( W = (/) -> ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w <-> E. n e. (/) ( W cyclShift n ) = w ) )
13 12 rabbidv 
 |-  ( W = (/) -> { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w e. Word V | E. n e. (/) ( W cyclShift n ) = w } )
14 rex0 
 |-  -. E. n e. (/) ( W cyclShift n ) = w
15 14 a1i 
 |-  ( W = (/) -> -. E. n e. (/) ( W cyclShift n ) = w )
16 15 ralrimivw 
 |-  ( W = (/) -> A. w e. Word V -. E. n e. (/) ( W cyclShift n ) = w )
17 rabeq0 
 |-  ( { w e. Word V | E. n e. (/) ( W cyclShift n ) = w } = (/) <-> A. w e. Word V -. E. n e. (/) ( W cyclShift n ) = w )
18 16 17 sylibr 
 |-  ( W = (/) -> { w e. Word V | E. n e. (/) ( W cyclShift n ) = w } = (/) )
19 13 18 eqtrd 
 |-  ( W = (/) -> { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = (/) )
20 1 19 eqtrid 
 |-  ( W = (/) -> M = (/) )
21 20 fveq2d 
 |-  ( W = (/) -> ( # ` M ) = ( # ` (/) ) )
22 hash0 
 |-  ( # ` (/) ) = 0
23 21 22 eqtrdi 
 |-  ( W = (/) -> ( # ` M ) = 0 )