pfxfvlsw

Description: The last symbol in a nonempty prefix of a word. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 3-May-2020)

		Ref	Expression
	Assertion	pfxfvlsw	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to lastS (W prefix L) = W (L - 1)$

Step	Hyp	Ref	Expression
1		pfxcl	$⊢ W \in Word V \to W prefix L \in Word V$
2	1	adantr	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to W prefix L \in Word V$
3		lsw	$⊢ W prefix L \in Word V \to lastS (W prefix L) = (W prefix L) (\|W prefix L\| - 1)$
4	2 3	syl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to lastS (W prefix L) = (W prefix L) (\|W prefix L\| - 1)$
5		fz1ssfz0	$⊢ (1 \dots \|W\|) \subseteq (0 \dots \|W\|)$
6	5	sseli	$⊢ L \in (1 \dots \|W\|) \to L \in (0 \dots \|W\|)$
7		pfxlen	$⊢ (W \in Word V \land L \in (0 \dots \|W\|)) \to \|W prefix L\| = L$
8	6 7	sylan2	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to \|W prefix L\| = L$
9	8	fvoveq1d	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to (W prefix L) (\|W prefix L\| - 1) = (W prefix L) (L - 1)$
10		simpl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to W \in Word V$
11	6	adantl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to L \in (0 \dots \|W\|)$
12		elfznn	$⊢ L \in (1 \dots \|W\|) \to L \in ℕ$
13		fzo0end	$⊢ L \in ℕ \to L - 1 \in (0 ..^L)$
14	12 13	syl	$⊢ L \in (1 \dots \|W\|) \to L - 1 \in (0 ..^L)$
15	14	adantl	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to L - 1 \in (0 ..^L)$
16		pfxfv	$⊢ (W \in Word V \land L \in (0 \dots \|W\|) \land L - 1 \in (0 ..^L)) \to (W prefix L) (L - 1) = W (L - 1)$
17	10 11 15 16	syl3anc	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to (W prefix L) (L - 1) = W (L - 1)$
18	4 9 17	3eqtrd	$⊢ (W \in Word V \land L \in (1 \dots \|W\|)) \to lastS (W prefix L) = W (L - 1)$

Metamath Proof Explorer