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

Metamath Proof Explorer

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 𝑁 ) = ∅