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 | |
|
Assertion | cshws0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cshwrepswhash1.m | |
|
2 | 0ex | |
|
3 | eleq1 | |
|
4 | 2 3 | mpbiri | |
5 | hasheq0 | |
|
6 | 5 | bicomd | |
7 | 4 6 | syl | |
8 | 7 | ibi | |
9 | 8 | oveq2d | |
10 | fzo0 | |
|
11 | 9 10 | eqtrdi | |
12 | 11 | rexeqdv | |
13 | 12 | rabbidv | |
14 | rex0 | |
|
15 | 14 | a1i | |
16 | 15 | ralrimivw | |
17 | rabeq0 | |
|
18 | 16 17 | sylibr | |
19 | 13 18 | eqtrd | |
20 | 1 19 | eqtrid | |
21 | 20 | fveq2d | |
22 | hash0 | |
|
23 | 21 22 | eqtrdi | |