Metamath Proof Explorer

Theorem pfxswrd

Description: A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018) (Revised by AV, 8-May-2020)

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

Proof

Step Hyp Ref Expression
1 ovexd 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( W substr <. M , N >. ) e. _V )
2 elfznn0 
 |-  ( L e. ( 0 ... ( N - M ) ) -> L e. NN0 )
3 pfxval 
 |-  ( ( ( W substr <. M , N >. ) e. _V /\ L e. NN0 ) -> ( ( W substr <. M , N >. ) prefix L ) = ( ( W substr <. M , N >. ) substr <. 0 , L >. ) )
4 1 2 3 syl2an 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( ( W substr <. M , N >. ) substr <. 0 , L >. ) )
5 fznn0sub 
 |-  ( M e. ( 0 ... N ) -> ( N - M ) e. NN0 )
6 5 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( N - M ) e. NN0 )
7 0elfz 
 |-  ( ( N - M ) e. NN0 -> 0 e. ( 0 ... ( N - M ) ) )
8 6 7 syl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> 0 e. ( 0 ... ( N - M ) ) )
9 8 anim1i 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( 0 e. ( 0 ... ( N - M ) ) /\ L e. ( 0 ... ( N - M ) ) ) )
10 swrdswrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( 0 e. ( 0 ... ( N - M ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) substr <. 0 , L >. ) = ( W substr <. ( M + 0 ) , ( M + L ) >. ) ) )
11 10 imp 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( 0 e. ( 0 ... ( N - M ) ) /\ L e. ( 0 ... ( N - M ) ) ) ) -> ( ( W substr <. M , N >. ) substr <. 0 , L >. ) = ( W substr <. ( M + 0 ) , ( M + L ) >. ) )
12 9 11 syldan 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) substr <. 0 , L >. ) = ( W substr <. ( M + 0 ) , ( M + L ) >. ) )
13 elfznn0 
 |-  ( M e. ( 0 ... N ) -> M e. NN0 )
14 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
15 14 addid1d 
 |-  ( M e. NN0 -> ( M + 0 ) = M )
16 13 15 syl 
 |-  ( M e. ( 0 ... N ) -> ( M + 0 ) = M )
17 16 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( M + 0 ) = M )
18 17 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( M + 0 ) = M )
19 18 opeq1d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> <. ( M + 0 ) , ( M + L ) >. = <. M , ( M + L ) >. )
20 19 oveq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( W substr <. ( M + 0 ) , ( M + L ) >. ) = ( W substr <. M , ( M + L ) >. ) )
21 4 12 20 3eqtrd 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ L e. ( 0 ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( W substr <. M , ( M + L ) >. ) )
22 21 ex 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - M ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( W substr <. M , ( M + L ) >. ) ) )