Theorem lsws3

Description: The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021)

	Ref	Expression
Assertion	lsws3	⊢ ( 𝐶 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		s3cli	⊢ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V
2		lsw	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word V → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) ) )
3	1 2	mp1i	⊢ ( 𝐶 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) ) )
4		s3len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
5	4	oveq1i	⊢ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) = ( 3 − 1 )
6		3m1e2	⊢ ( 3 − 1 ) = 2
7	5 6	eqtri	⊢ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) = 2
8	7	fveq2i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 )
9	8	a1i	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) − 1 ) ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) )
10		s3fv2	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
11	3 9 10	3eqtrd	⊢ ( 𝐶 ∈ 𝑉 → ( lastS ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 𝐶 )