Theorem 0csh0

Description: Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018) (Revised by AV, 17-Nov-2018)

	Ref	Expression
Assertion	0csh0	⊢ ( ∅ cyclShift 𝑁 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-csh	⊢ cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
2	1	a1i	⊢ ( 𝑁 ∈ ℤ → cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) ) )
3		iftrue	⊢ ( 𝑤 = ∅ → if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) = ∅ )
4	3	ad2antrl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑤 = ∅ ∧ 𝑛 = 𝑁 ) ) → if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) = ∅ )
5		0nn0	⊢ 0 ∈ ℕ0
6		f0	⊢ ∅ : ∅ ⟶ V
7		ffn	⊢ ( ∅ : ∅ ⟶ V → ∅ Fn ∅ )
8		fzo0	⊢ ( 0 ..^ 0 ) = ∅
9	8	eqcomi	⊢ ∅ = ( 0 ..^ 0 )
10	9	fneq2i	⊢ ( ∅ Fn ∅ ↔ ∅ Fn ( 0 ..^ 0 ) )
11	7 10	sylib	⊢ ( ∅ : ∅ ⟶ V → ∅ Fn ( 0 ..^ 0 ) )
12	6 11	ax-mp	⊢ ∅ Fn ( 0 ..^ 0 )
13		id	⊢ ( 0 ∈ ℕ0 → 0 ∈ ℕ0 )
14		oveq2	⊢ ( 𝑙 = 0 → ( 0 ..^ 𝑙 ) = ( 0 ..^ 0 ) )
15	14	fneq2d	⊢ ( 𝑙 = 0 → ( ∅ Fn ( 0 ..^ 𝑙 ) ↔ ∅ Fn ( 0 ..^ 0 ) ) )
16	15	adantl	⊢ ( ( 0 ∈ ℕ0 ∧ 𝑙 = 0 ) → ( ∅ Fn ( 0 ..^ 𝑙 ) ↔ ∅ Fn ( 0 ..^ 0 ) ) )
17	13 16	rspcedv	⊢ ( 0 ∈ ℕ0 → ( ∅ Fn ( 0 ..^ 0 ) → ∃ 𝑙 ∈ ℕ0 ∅ Fn ( 0 ..^ 𝑙 ) ) )
18	5 12 17	mp2	⊢ ∃ 𝑙 ∈ ℕ0 ∅ Fn ( 0 ..^ 𝑙 )
19		0ex	⊢ ∅ ∈ V
20		fneq1	⊢ ( 𝑓 = ∅ → ( 𝑓 Fn ( 0 ..^ 𝑙 ) ↔ ∅ Fn ( 0 ..^ 𝑙 ) ) )
21	20	rexbidv	⊢ ( 𝑓 = ∅ → ( ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) ↔ ∃ 𝑙 ∈ ℕ0 ∅ Fn ( 0 ..^ 𝑙 ) ) )
22	19 21	elab	⊢ ( ∅ ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ↔ ∃ 𝑙 ∈ ℕ0 ∅ Fn ( 0 ..^ 𝑙 ) )
23	18 22	mpbir	⊢ ∅ ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) }
24	23	a1i	⊢ ( 𝑁 ∈ ℤ → ∅ ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } )
25		id	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
26	19	a1i	⊢ ( 𝑁 ∈ ℤ → ∅ ∈ V )
27	2 4 24 25 26	ovmpod	⊢ ( 𝑁 ∈ ℤ → ( ∅ cyclShift 𝑁 ) = ∅ )
28		cshnz	⊢ ( ¬ 𝑁 ∈ ℤ → ( ∅ cyclShift 𝑁 ) = ∅ )
29	27 28	pm2.61i	⊢ ( ∅ cyclShift 𝑁 ) = ∅