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 ) >. ) ) )