Theorem addlenrevpfx

Description: The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 3-May-2020)

	Ref	Expression
Assertion	addlenrevpfx	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( # ` W ) )

Proof

Step	Hyp	Ref	Expression
1		swrdrlen	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , ( # ` W ) >. ) ) = ( ( # ` W ) - M ) )
2		pfxlen	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) = M )
3	1 2	oveq12d	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( ( ( # ` W ) - M ) + M ) )
4		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
5		elfzelz	|- ( M e. ( 0 ... ( # ` W ) ) -> M e. ZZ )
6		nn0cn	|- ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
7		zcn	|- ( M e. ZZ -> M e. CC )
8		npcan	|- ( ( ( # ` W ) e. CC /\ M e. CC ) -> ( ( ( # ` W ) - M ) + M ) = ( # ` W ) )
9	6 7 8	syl2an	|- ( ( ( # ` W ) e. NN0 /\ M e. ZZ ) -> ( ( ( # ` W ) - M ) + M ) = ( # ` W ) )
10	4 5 9	syl2an	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( ( # ` W ) - M ) + M ) = ( # ` W ) )
11	3 10	eqtrd	|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( # ` W ) )