Metamath Proof Explorer

Theorem ccatval1lsw

Description: The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatval1lsw 
|- ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )

Proof

Step Hyp Ref Expression
1 lennncl 
 |-  ( ( A e. Word V /\ A =/= (/) ) -> ( # ` A ) e. NN )
2 1 3adant2 
 |-  ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( # ` A ) e. NN )
3 fzo0end 
 |-  ( ( # ` A ) e. NN -> ( ( # ` A ) - 1 ) e. ( 0 ..^ ( # ` A ) ) )
4 2 3 syl 
 |-  ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( # ` A ) - 1 ) e. ( 0 ..^ ( # ` A ) ) )
5 ccatval1 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( ( # ` A ) - 1 ) e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( A ` ( ( # ` A ) - 1 ) ) )
6 4 5 syld3an3 
 |-  ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( A ` ( ( # ` A ) - 1 ) ) )
7 lsw 
 |-  ( A e. Word V -> ( lastS ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
8 7 3ad2ant1 
 |-  ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( lastS ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
9 6 8 eqtr4d 
 |-  ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )