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 )