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 ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
Assertion cshws0 ⊢ W = ∅ → M = 0

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
2 0ex ⊢ ∅ ∈ V
3 eleq1 ⊢ W = ∅ → W ∈ V ↔ ∅ ∈ V
4 2 3 mpbiri ⊢ W = ∅ → W ∈ V
5 hasheq0 ⊢ W ∈ V → W = 0 ↔ W = ∅
6 5 bicomd ⊢ W ∈ 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 = ∅ → ∃ n ∈ 0 ..^ W W cyclShift n = w ↔ ∃ n ∈ ∅ W cyclShift n = w
13 12 rabbidv ⊢ W = ∅ → w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = w ∈ Word V | ∃ n ∈ ∅ W cyclShift n = w
14 rex0 ⊢ ¬ ∃ n ∈ ∅ W cyclShift n = w
15 14 a1i ⊢ W = ∅ → ¬ ∃ n ∈ ∅ W cyclShift n = w
16 15 ralrimivw ⊢ W = ∅ → ∀ w ∈ Word V ¬ ∃ n ∈ ∅ W cyclShift n = w
17 rabeq0 ⊢ w ∈ Word V | ∃ n ∈ ∅ W cyclShift n = w = ∅ ↔ ∀ w ∈ Word V ¬ ∃ n ∈ ∅ W cyclShift n = w
18 16 17 sylibr ⊢ W = ∅ → w ∈ Word V | ∃ n ∈ ∅ W cyclShift n = w = ∅
19 13 18 eqtrd ⊢ W = ∅ → w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = ∅
20 1 19 syl5eq ⊢ W = ∅ → M = ∅
21 20 fveq2d ⊢ W = ∅ → M = ∅
22 hash0 ⊢ ∅ = 0
23 21 22 eqtrdi ⊢ W = ∅ → M = 0