This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshws0 ( 𝑊 = ∅ → ( ♯ ‘ 𝑀 ) = 0 )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 0ex ⊢ ∅ ∈ V
3 eleq1 ⊢ ( 𝑊 = ∅ → ( 𝑊 ∈ V ↔ ∅ ∈ V ) )
4 2 3 mpbiri ⊢ ( 𝑊 = ∅ → 𝑊 ∈ V )
5 hasheq0 ⊢ ( 𝑊 ∈ V → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
6 5 bicomd ⊢ ( 𝑊 ∈ V → ( 𝑊 = ∅ ↔ ( ♯ ‘ 𝑊 ) = 0 ) )
7 4 6 syl ⊢ ( 𝑊 = ∅ → ( 𝑊 = ∅ ↔ ( ♯ ‘ 𝑊 ) = 0 ) )
8 7 ibi ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = 0 )
9 8 oveq2d ⊢ ( 𝑊 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 0 ) )
10 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
11 9 10 eqtrdi ⊢ ( 𝑊 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ∅ )
12 11 rexeqdv ⊢ ( 𝑊 = ∅ → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) )
13 12 rabbidv ⊢ ( 𝑊 = ∅ → { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 } )
14 rex0 ⊢ ¬ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤
15 14 a1i ⊢ ( 𝑊 = ∅ → ¬ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
16 15 ralrimivw ⊢ ( 𝑊 = ∅ → ∀ 𝑤 ∈ Word 𝑉 ¬ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
17 rabeq0 ⊢ ( { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = ∅ ↔ ∀ 𝑤 ∈ Word 𝑉 ¬ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
18 16 17 sylibr ⊢ ( 𝑊 = ∅ → { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ∅ ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = ∅ )
19 13 18 eqtrd ⊢ ( 𝑊 = ∅ → { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = ∅ )
20 1 19 eqtrid ⊢ ( 𝑊 = ∅ → 𝑀 = ∅ )
21 20 fveq2d ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ ∅ ) )
22 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
23 21 22 eqtrdi ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑀 ) = 0 )