Metamath Proof Explorer


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 ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 𝐶 )