Metamath Proof Explorer

Theorem lsws4

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

Ref Expression
Assertion lsws4 
|- ( D e. V -> ( lastS ` <" A B C D "> ) = D )

Proof

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