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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pfxcl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 )
2	1	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 )
3		lsw	⊢ ( ( 𝑊 prefix 𝐿 ) ∈ Word 𝑉 → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) )
4	2 3	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) )
5		fz1ssfz0	⊢ ( 1 ... ( ♯ ‘ 𝑊 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝑊 ) )
6	5	sseli	⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
7		pfxlen	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) = 𝐿 )
8	6 7	sylan2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) = 𝐿 )
9	8	fvoveq1d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( ( ♯ ‘ ( 𝑊 prefix 𝐿 ) ) − 1 ) ) = ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) )
10		simpl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
11	6	adantl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
12		elfznn	⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ )
13		fzo0end	⊢ ( 𝐿 ∈ ℕ → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
14	12 13	syl	⊢ ( 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
15	14	adantl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) )
16		pfxfv	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐿 − 1 ) ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )
17	10 11 15 16	syl3anc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐿 ) ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )
18	4 9 17	3eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix 𝐿 ) ) = ( 𝑊 ‘ ( 𝐿 − 1 ) ) )