Metamath Proof Explorer

Theorem lenrevpfxcctswrd

Description: The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 9-May-2020)

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

Proof

Step Hyp Ref Expression
1 swrdcl 
 |-  ( W e. Word V -> ( W substr <. M , ( # ` W ) >. ) e. Word V )
2 pfxcl 
 |-  ( W e. Word V -> ( W prefix M ) e. Word V )
3 ccatlen 
 |-  ( ( ( W substr <. M , ( # ` W ) >. ) e. Word V /\ ( W prefix M ) e. Word V ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) )
4 1 2 3 syl2anc 
 |-  ( W e. Word V -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) )
5 4 adantr 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) )
6 swrdrlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , ( # ` W ) >. ) ) = ( ( # ` W ) - M ) )
7 fznn0sub 
 |-  ( M e. ( 0 ... ( # ` W ) ) -> ( ( # ` W ) - M ) e. NN0 )
8 7 adantl 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` W ) - M ) e. NN0 )
9 6 8 eqeltrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , ( # ` W ) >. ) ) e. NN0 )
10 9 nn0cnd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , ( # ` W ) >. ) ) e. CC )
11 pfxlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) = M )
12 elfznn0 
 |-  ( M e. ( 0 ... ( # ` W ) ) -> M e. NN0 )
13 12 adantl 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> M e. NN0 )
14 11 13 eqeltrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) e. NN0 )
15 14 nn0cnd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) e. CC )
16 10 15 addcomd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( ( # ` ( W prefix M ) ) + ( # ` ( W substr <. M , ( # ` W ) >. ) ) ) )
17 addlenpfx 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W prefix M ) ) + ( # ` ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )
18 5 16 17 3eqtrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( # ` W ) )