Step |
Hyp |
Ref |
Expression |
1 |
|
swrdf1.w |
|- ( ph -> W e. Word D ) |
2 |
|
swrdf1.m |
|- ( ph -> M e. ( 0 ... N ) ) |
3 |
|
swrdf1.n |
|- ( ph -> N e. ( 0 ... ( # ` W ) ) ) |
4 |
|
swrdf1.1 |
|- ( ph -> W : dom W -1-1-> D ) |
5 |
|
swrdrndisj.1 |
|- ( ph -> O e. ( N ... P ) ) |
6 |
|
swrdrndisj.2 |
|- ( ph -> P e. ( N ... ( # ` W ) ) ) |
7 |
|
swrdrn3 |
|- ( ( W e. Word D /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) = ( W " ( M ..^ N ) ) ) |
8 |
1 2 3 7
|
syl3anc |
|- ( ph -> ran ( W substr <. M , N >. ) = ( W " ( M ..^ N ) ) ) |
9 |
|
elfzuz |
|- ( N e. ( 0 ... ( # ` W ) ) -> N e. ( ZZ>= ` 0 ) ) |
10 |
|
fzss1 |
|- ( N e. ( ZZ>= ` 0 ) -> ( N ... P ) C_ ( 0 ... P ) ) |
11 |
3 9 10
|
3syl |
|- ( ph -> ( N ... P ) C_ ( 0 ... P ) ) |
12 |
11 5
|
sseldd |
|- ( ph -> O e. ( 0 ... P ) ) |
13 |
|
fzss1 |
|- ( N e. ( ZZ>= ` 0 ) -> ( N ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) ) ) |
14 |
3 9 13
|
3syl |
|- ( ph -> ( N ... ( # ` W ) ) C_ ( 0 ... ( # ` W ) ) ) |
15 |
14 6
|
sseldd |
|- ( ph -> P e. ( 0 ... ( # ` W ) ) ) |
16 |
|
swrdrn3 |
|- ( ( W e. Word D /\ O e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. O , P >. ) = ( W " ( O ..^ P ) ) ) |
17 |
1 12 15 16
|
syl3anc |
|- ( ph -> ran ( W substr <. O , P >. ) = ( W " ( O ..^ P ) ) ) |
18 |
8 17
|
ineq12d |
|- ( ph -> ( ran ( W substr <. M , N >. ) i^i ran ( W substr <. O , P >. ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) ) |
19 |
|
df-f1 |
|- ( W : dom W -1-1-> D <-> ( W : dom W --> D /\ Fun `' W ) ) |
20 |
19
|
simprbi |
|- ( W : dom W -1-1-> D -> Fun `' W ) |
21 |
|
imain |
|- ( Fun `' W -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) ) |
22 |
4 20 21
|
3syl |
|- ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( ( W " ( M ..^ N ) ) i^i ( W " ( O ..^ P ) ) ) ) |
23 |
|
elfzuz |
|- ( O e. ( N ... P ) -> O e. ( ZZ>= ` N ) ) |
24 |
|
fzoss1 |
|- ( O e. ( ZZ>= ` N ) -> ( O ..^ P ) C_ ( N ..^ P ) ) |
25 |
5 23 24
|
3syl |
|- ( ph -> ( O ..^ P ) C_ ( N ..^ P ) ) |
26 |
|
elfzuz3 |
|- ( P e. ( N ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` P ) ) |
27 |
|
fzoss2 |
|- ( ( # ` W ) e. ( ZZ>= ` P ) -> ( N ..^ P ) C_ ( N ..^ ( # ` W ) ) ) |
28 |
6 26 27
|
3syl |
|- ( ph -> ( N ..^ P ) C_ ( N ..^ ( # ` W ) ) ) |
29 |
25 28
|
sstrd |
|- ( ph -> ( O ..^ P ) C_ ( N ..^ ( # ` W ) ) ) |
30 |
|
sslin |
|- ( ( O ..^ P ) C_ ( N ..^ ( # ` W ) ) -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) ) |
31 |
29 30
|
syl |
|- ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) ) |
32 |
|
fzodisj |
|- ( ( M ..^ N ) i^i ( N ..^ ( # ` W ) ) ) = (/) |
33 |
31 32
|
sseqtrdi |
|- ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ (/) ) |
34 |
|
ss0 |
|- ( ( ( M ..^ N ) i^i ( O ..^ P ) ) C_ (/) -> ( ( M ..^ N ) i^i ( O ..^ P ) ) = (/) ) |
35 |
33 34
|
syl |
|- ( ph -> ( ( M ..^ N ) i^i ( O ..^ P ) ) = (/) ) |
36 |
35
|
imaeq2d |
|- ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = ( W " (/) ) ) |
37 |
|
ima0 |
|- ( W " (/) ) = (/) |
38 |
36 37
|
eqtrdi |
|- ( ph -> ( W " ( ( M ..^ N ) i^i ( O ..^ P ) ) ) = (/) ) |
39 |
18 22 38
|
3eqtr2d |
|- ( ph -> ( ran ( W substr <. M , N >. ) i^i ran ( W substr <. O , P >. ) ) = (/) ) |