This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsws2

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

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

Proof

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