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