Theorem lsw0

Description: The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018) (Proof shortened by AV, 2-May-2020)

	Ref	Expression
Assertion	lsw0	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		lsw	⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
2	1	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
3		fvoveq1	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 0 − 1 ) ) )
4		wrddm	⊢ ( 𝑊 ∈ Word 𝑉 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5		1nn	⊢ 1 ∈ ℕ
6		nnnle0	⊢ ( 1 ∈ ℕ → ¬ 1 ≤ 0 )
7	5 6	ax-mp	⊢ ¬ 1 ≤ 0
8		0re	⊢ 0 ∈ ℝ
9		1re	⊢ 1 ∈ ℝ
10	8 9	subge0i	⊢ ( 0 ≤ ( 0 − 1 ) ↔ 1 ≤ 0 )
11	7 10	mtbir	⊢ ¬ 0 ≤ ( 0 − 1 )
12		elfzole1	⊢ ( ( 0 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 0 ≤ ( 0 − 1 ) )
13	11 12	mto	⊢ ¬ ( 0 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) )
14		eleq2	⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 0 − 1 ) ∈ dom 𝑊 ↔ ( 0 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
15	13 14	mtbiri	⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ¬ ( 0 − 1 ) ∈ dom 𝑊 )
16		ndmfv	⊢ ( ¬ ( 0 − 1 ) ∈ dom 𝑊 → ( 𝑊 ‘ ( 0 − 1 ) ) = ∅ )
17	4 15 16	3syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ‘ ( 0 − 1 ) ) = ∅ )
18	3 17	sylan9eqr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ∅ )
19	2 18	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( lastS ‘ 𝑊 ) = ∅ )