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 )