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=wWordV|n0..^WWcyclShiftn=w
Assertion cshws0 W=M=0

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m M=wWordV|n0..^WWcyclShiftn=w
2 0ex V
3 eleq1 W=WVV
4 2 3 mpbiri W=WV
5 hasheq0 WVW=0W=
6 5 bicomd WVW=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=n0..^WWcyclShiftn=wnWcyclShiftn=w
13 12 rabbidv W=wWordV|n0..^WWcyclShiftn=w=wWordV|nWcyclShiftn=w
14 rex0 ¬nWcyclShiftn=w
15 14 a1i W=¬nWcyclShiftn=w
16 15 ralrimivw W=wWordV¬nWcyclShiftn=w
17 rabeq0 wWordV|nWcyclShiftn=w=wWordV¬nWcyclShiftn=w
18 16 17 sylibr W=wWordV|nWcyclShiftn=w=
19 13 18 eqtrd W=wWordV|n0..^WWcyclShiftn=w=
20 1 19 eqtrid W=M=
21 20 fveq2d W=M=
22 hash0 =0
23 21 22 eqtrdi W=M=0