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 syl6eq ( 𝑊 = ∅ → ( 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 syl5eq ( 𝑊 = ∅ → 𝑀 = ∅ )
21 20 fveq2d ( 𝑊 = ∅ → ( ♯ ‘ 𝑀 ) = ( ♯ ‘ ∅ ) )
22 hash0 ( ♯ ‘ ∅ ) = 0
23 21 22 syl6eq ( 𝑊 = ∅ → ( ♯ ‘ 𝑀 ) = 0 )