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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ ) → ( ( 𝐼 < 0 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐼 ) → ( 𝑊 ‘ 𝐼 ) = ∅ ) )

Proof

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