Metamath Proof Explorer

Theorem wrdsymb0

Description: A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion wrdsymb0 ⊢ W ∈ Word V ∧ I ∈ ℤ → I < 0 ∨ W ≤ I → W ⁡ I = ∅

Proof

Step Hyp Ref Expression
1 wrddm ⊢ W ∈ Word V → dom ⁡ W = 0 ..^ W
2 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
3 2 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
4 simpr ⊢ W ∈ ℤ ∧ I ∈ ℤ → I ∈ ℤ
5 0zd ⊢ W ∈ ℤ ∧ I ∈ ℤ → 0 ∈ ℤ
6 simpl ⊢ W ∈ ℤ ∧ I ∈ ℤ → W ∈ ℤ
7 nelfzo ⊢ I ∈ ℤ ∧ 0 ∈ ℤ ∧ W ∈ ℤ → I ∉ 0 ..^ W ↔ I < 0 ∨ W ≤ I
8 4 5 6 7 syl3anc ⊢ W ∈ ℤ ∧ I ∈ ℤ → I ∉ 0 ..^ W ↔ I < 0 ∨ W ≤ I
9 8 biimpar ⊢ W ∈ ℤ ∧ I ∈ ℤ ∧ I < 0 ∨ W ≤ I → I ∉ 0 ..^ W
10 df-nel ⊢ I ∉ 0 ..^ W ↔ ¬ I ∈ 0 ..^ W
11 9 10 sylib ⊢ W ∈ ℤ ∧ I ∈ ℤ ∧ I < 0 ∨ W ≤ I → ¬ I ∈ 0 ..^ W
12 eleq2 ⊢ dom ⁡ W = 0 ..^ W → I ∈ dom ⁡ W ↔ I ∈ 0 ..^ W
13 12 notbid ⊢ dom ⁡ W = 0 ..^ W → ¬ I ∈ dom ⁡ W ↔ ¬ I ∈ 0 ..^ W
14 11 13 imbitrrid ⊢ dom ⁡ W = 0 ..^ W → W ∈ ℤ ∧ I ∈ ℤ ∧ I < 0 ∨ W ≤ I → ¬ I ∈ dom ⁡ W
15 14 exp4c ⊢ dom ⁡ W = 0 ..^ W → W ∈ ℤ → I ∈ ℤ → I < 0 ∨ W ≤ I → ¬ I ∈ dom ⁡ W
16 1 3 15 sylc ⊢ W ∈ Word V → I ∈ ℤ → I < 0 ∨ W ≤ I → ¬ I ∈ dom ⁡ W
17 16 imp ⊢ W ∈ Word V ∧ I ∈ ℤ → I < 0 ∨ W ≤ I → ¬ I ∈ dom ⁡ W
18 ndmfv ⊢ ¬ I ∈ dom ⁡ W → W ⁡ I = ∅
19 17 18 syl6 ⊢ W ∈ Word V ∧ I ∈ ℤ → I < 0 ∨ W ≤ I → W ⁡ I = ∅