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 )