Step |
Hyp |
Ref |
Expression |
1 |
|
elfznn0 |
|- ( L e. ( 0 ... ( # ` W ) ) -> L e. NN0 ) |
2 |
|
pfxval |
|- ( ( W e. Word V /\ L e. NN0 ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) ) |
3 |
1 2
|
sylan2 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) ) |
4 |
3
|
3adant3 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) ) |
5 |
4
|
fveq1d |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` I ) = ( ( W substr <. 0 , L >. ) ` I ) ) |
6 |
|
simp1 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> W e. Word V ) |
7 |
|
0elfz |
|- ( L e. NN0 -> 0 e. ( 0 ... L ) ) |
8 |
1 7
|
syl |
|- ( L e. ( 0 ... ( # ` W ) ) -> 0 e. ( 0 ... L ) ) |
9 |
8
|
3ad2ant2 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> 0 e. ( 0 ... L ) ) |
10 |
|
simp2 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> L e. ( 0 ... ( # ` W ) ) ) |
11 |
1
|
nn0cnd |
|- ( L e. ( 0 ... ( # ` W ) ) -> L e. CC ) |
12 |
11
|
subid1d |
|- ( L e. ( 0 ... ( # ` W ) ) -> ( L - 0 ) = L ) |
13 |
12
|
eqcomd |
|- ( L e. ( 0 ... ( # ` W ) ) -> L = ( L - 0 ) ) |
14 |
13
|
oveq2d |
|- ( L e. ( 0 ... ( # ` W ) ) -> ( 0 ..^ L ) = ( 0 ..^ ( L - 0 ) ) ) |
15 |
14
|
eleq2d |
|- ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) <-> I e. ( 0 ..^ ( L - 0 ) ) ) ) |
16 |
15
|
biimpd |
|- ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) -> I e. ( 0 ..^ ( L - 0 ) ) ) ) |
17 |
16
|
a1i |
|- ( W e. Word V -> ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) -> I e. ( 0 ..^ ( L - 0 ) ) ) ) ) |
18 |
17
|
3imp |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> I e. ( 0 ..^ ( L - 0 ) ) ) |
19 |
|
swrdfv |
|- ( ( ( W e. Word V /\ 0 e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) /\ I e. ( 0 ..^ ( L - 0 ) ) ) -> ( ( W substr <. 0 , L >. ) ` I ) = ( W ` ( I + 0 ) ) ) |
20 |
6 9 10 18 19
|
syl31anc |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W substr <. 0 , L >. ) ` I ) = ( W ` ( I + 0 ) ) ) |
21 |
|
elfzoelz |
|- ( I e. ( 0 ..^ L ) -> I e. ZZ ) |
22 |
21
|
zcnd |
|- ( I e. ( 0 ..^ L ) -> I e. CC ) |
23 |
22
|
addid1d |
|- ( I e. ( 0 ..^ L ) -> ( I + 0 ) = I ) |
24 |
23
|
3ad2ant3 |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( I + 0 ) = I ) |
25 |
24
|
fveq2d |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( W ` ( I + 0 ) ) = ( W ` I ) ) |
26 |
5 20 25
|
3eqtrd |
|- ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` I ) = ( W ` I ) ) |