Theorem pfxtrcfvl

Description: The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018) (Revised by AV, 5-May-2020)

	Ref	Expression
Assertion	pfxtrcfvl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	a1i	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℤ )
3		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4	3	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
5	4	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
6		simpr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
7		eluz2	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
8	2 5 6 7	syl3anbrc	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
9		ige2m1fz1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
10	8 9	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
11		pfxfvlsw	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
12	10 11	syldan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
13	3	nn0cnd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
14		sub1m1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
15	13 14	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
16	15	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
17	16	fveq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
18	12 17	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )