Theorem 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 e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pfxcl	|- ( W e. Word V -> ( W prefix L ) e. Word V )
2	1	adantr	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( W prefix L ) e. Word V )
3		lsw	|- ( ( W prefix L ) e. Word V -> ( lastS ` ( W prefix L ) ) = ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) )
4	2 3	syl	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) )
5		fz1ssfz0	|- ( 1 ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) )
6	5	sseli	|- ( L e. ( 1 ... ( # ` W ) ) -> L e. ( 0 ... ( # ` W ) ) )
7		pfxlen	|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
8	6 7	sylan2	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( # ` ( W prefix L ) ) = L )
9	8	fvoveq1d	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` ( ( # ` ( W prefix L ) ) - 1 ) ) = ( ( W prefix L ) ` ( L - 1 ) ) )
10		simpl	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> W e. Word V )
11	6	adantl	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> L e. ( 0 ... ( # ` W ) ) )
12		elfznn	|- ( L e. ( 1 ... ( # ` W ) ) -> L e. NN )
13		fzo0end	|- ( L e. NN -> ( L - 1 ) e. ( 0 ..^ L ) )
14	12 13	syl	|- ( L e. ( 1 ... ( # ` W ) ) -> ( L - 1 ) e. ( 0 ..^ L ) )
15	14	adantl	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( L - 1 ) e. ( 0 ..^ L ) )
16		pfxfv	|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ ( L - 1 ) e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` ( L - 1 ) ) = ( W ` ( L - 1 ) ) )
17	10 11 15 16	syl3anc	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix L ) ` ( L - 1 ) ) = ( W ` ( L - 1 ) ) )
18	4 9 17	3eqtrd	|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )