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
|- ( C e. V -> ( lastS ` <" A B C "> ) = C )

Proof

Step Hyp Ref Expression
1 s3cli
 |-  <" A B C "> e. Word _V
2 lsw
 |-  ( <" A B C "> e. Word _V -> ( lastS ` <" A B C "> ) = ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) )
3 1 2 mp1i
 |-  ( C e. V -> ( lastS ` <" A B C "> ) = ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) )
4 s3len
 |-  ( # ` <" A B C "> ) = 3
5 4 oveq1i
 |-  ( ( # ` <" A B C "> ) - 1 ) = ( 3 - 1 )
6 3m1e2
 |-  ( 3 - 1 ) = 2
7 5 6 eqtri
 |-  ( ( # ` <" A B C "> ) - 1 ) = 2
8 7 fveq2i
 |-  ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) = ( <" A B C "> ` 2 )
9 8 a1i
 |-  ( C e. V -> ( <" A B C "> ` ( ( # ` <" A B C "> ) - 1 ) ) = ( <" A B C "> ` 2 ) )
10 s3fv2
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )
11 3 9 10 3eqtrd
 |-  ( C e. V -> ( lastS ` <" A B C "> ) = C )