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	syl5ibr	⊢ ( 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 ∨ ( ♯ ‘ 𝑊 ) ≤ 𝐼 ) → ( 𝑊 ‘ 𝐼 ) = ∅ ) )