Metamath Proof Explorer

Theorem addlenpfx

Description: The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018) (Revised by AV, 3-May-2020)

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

Proof

Step Hyp Ref Expression
1 pfxlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) = M )
2 swrdrlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , ( # ` W ) >. ) ) = ( ( # ` W ) - M ) )
3 1 2 oveq12d 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix M ) ) + ( # ` ( W substr <. M , ( # ` W ) >. ) ) ) = ( M + ( ( # ` W ) - M ) ) )
4 elfznn0 
 |-  ( M e. ( 0 ... ( # ` W ) ) -> M e. NN0 )
5 4 nn0cnd 
 |-  ( M e. ( 0 ... ( # ` W ) ) -> M e. CC )
6 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
7 6 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
8 pncan3 
 |-  ( ( M e. CC /\ ( # ` W ) e. CC ) -> ( M + ( ( # ` W ) - M ) ) = ( # ` W ) )
9 5 7 8 syl2anr 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( M + ( ( # ` W ) - M ) ) = ( # ` W ) )
10 3 9 eqtrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix M ) ) + ( # ` ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )