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 N = ∅

Proof

Step Hyp Ref Expression
1 df-csh ⊢ cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
2 1 a1i ⊢ N ∈ ℤ → cyclShift = w ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l , n ∈ ℤ ⟼ if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w
3 iftrue ⊢ w = ∅ → if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w = ∅
4 3 ad2antrl ⊢ N ∈ ℤ ∧ w = ∅ ∧ n = N → if w = ∅ ∅ w substr n mod w w ++ w prefix n mod w = ∅
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 ⊢ l = 0 → 0 ..^ l = 0 ..^ 0
15 14 fneq2d ⊢ l = 0 → ∅ Fn 0 ..^ l ↔ ∅ Fn 0 ..^ 0
16 15 adantl ⊢ 0 ∈ ℕ 0 ∧ l = 0 → ∅ Fn 0 ..^ l ↔ ∅ Fn 0 ..^ 0
17 13 16 rspcedv ⊢ 0 ∈ ℕ 0 → ∅ Fn 0 ..^ 0 → ∃ l ∈ ℕ 0 ∅ Fn 0 ..^ l
18 5 12 17 mp2 ⊢ ∃ l ∈ ℕ 0 ∅ Fn 0 ..^ l
19 0ex ⊢ ∅ ∈ V
20 fneq1 ⊢ f = ∅ → f Fn 0 ..^ l ↔ ∅ Fn 0 ..^ l
21 20 rexbidv ⊢ f = ∅ → ∃ l ∈ ℕ 0 f Fn 0 ..^ l ↔ ∃ l ∈ ℕ 0 ∅ Fn 0 ..^ l
22 19 21 elab ⊢ ∅ ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l ↔ ∃ l ∈ ℕ 0 ∅ Fn 0 ..^ l
23 18 22 mpbir ⊢ ∅ ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l
24 23 a1i ⊢ N ∈ ℤ → ∅ ∈ f | ∃ l ∈ ℕ 0 f Fn 0 ..^ l
25 id ⊢ N ∈ ℤ → N ∈ ℤ
26 19 a1i ⊢ N ∈ ℤ → ∅ ∈ V
27 2 4 24 25 26 ovmpod ⊢ N ∈ ℤ → ∅ cyclShift N = ∅
28 cshnz ⊢ ¬ N ∈ ℤ → ∅ cyclShift N = ∅
29 27 28 pm2.61i ⊢ ∅ cyclShift N = ∅