Metamath Proof Explorer

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	$⊢ (W \in Word V \land \|W\| = 0) \to lastS (W) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		lsw	$⊢ W \in Word V \to lastS (W) = W (\|W\| - 1)$
2	1	adantr	$⊢ (W \in Word V \land \|W\| = 0) \to lastS (W) = W (\|W\| - 1)$
3		fvoveq1	$⊢ \|W\| = 0 \to W (\|W\| - 1) = W (0 - 1)$
4		wrddm	$⊢ W \in Word V \to dom W = (0 ..^\|W\|)$
5		1nn	$⊢ 1 \in ℕ$
6		nnnle0	$⊢ 1 \in ℕ \to \neg 1 \leq 0$
7	5 6	ax-mp	$⊢ \neg 1 \leq 0$
8		0re	$⊢ 0 \in ℝ$
9		1re	$⊢ 1 \in ℝ$
10	8 9	subge0i	$⊢ 0 \leq 0 - 1 \leftrightarrow 1 \leq 0$
11	7 10	mtbir	$⊢ \neg 0 \leq 0 - 1$
12		elfzole1	$⊢ 0 - 1 \in (0 ..^\|W\|) \to 0 \leq 0 - 1$
13	11 12	mto	$⊢ \neg 0 - 1 \in (0 ..^\|W\|)$
14		eleq2	$⊢ dom W = (0 ..^\|W\|) \to (0 - 1 \in dom W \leftrightarrow 0 - 1 \in (0 ..^\|W\|))$
15	13 14	mtbiri	$⊢ dom W = (0 ..^\|W\|) \to \neg 0 - 1 \in dom W$
16		ndmfv	$⊢ \neg 0 - 1 \in dom W \to W (0 - 1) = \emptyset$
17	4 15 16	3syl	$⊢ W \in Word V \to W (0 - 1) = \emptyset$
18	3 17	sylan9eqr	$⊢ (W \in Word V \land \|W\| = 0) \to W (\|W\| - 1) = \emptyset$
19	2 18	eqtrd	$⊢ (W \in Word V \land \|W\| = 0) \to lastS (W) = \emptyset$