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 addlenrevpfx 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( # ` ( W substr <. M , ( # ` W ) >. ) ) + ( # ` ( W prefix M ) ) ) = ( # ` W ) )
7 5 6 eqtrd 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( # ` W ) )