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

Metamath Proof Explorer

Theorem pfxlswccat

Description: Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion pfxlswccat 
|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )

Proof

Step Hyp Ref Expression
1 swrdlsw 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )
2 1 eqcomd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> <" ( lastS ` W ) "> = ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) )
3 2 oveq2d 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = ( ( W prefix ( ( # ` W ) - 1 ) ) ++ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) )
4 wrdfin 
 |-  ( W e. Word V -> W e. Fin )
5 1elfz0hash 
 |-  ( ( W e. Fin /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
6 4 5 sylan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
7 fznn0sub2 
 |-  ( 1 e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
8 6 7 syl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
9 pfxcctswrd 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) = W )
10 8 9 syldan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) ) = W )
11 3 10 eqtrd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )