Step |
Hyp |
Ref |
Expression |
1 |
|
deg1submon1p.d |
|- D = ( deg1 ` R ) |
2 |
|
deg1submon1p.o |
|- O = ( Monic1p ` R ) |
3 |
|
deg1submon1p.p |
|- P = ( Poly1 ` R ) |
4 |
|
deg1submon1p.m |
|- .- = ( -g ` P ) |
5 |
|
deg1submon1p.r |
|- ( ph -> R e. Ring ) |
6 |
|
deg1submon1p.f1 |
|- ( ph -> F e. O ) |
7 |
|
deg1submon1p.f2 |
|- ( ph -> ( D ` F ) = X ) |
8 |
|
deg1submon1p.g1 |
|- ( ph -> G e. O ) |
9 |
|
deg1submon1p.g2 |
|- ( ph -> ( D ` G ) = X ) |
10 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
11 |
3 10 2
|
mon1pcl |
|- ( F e. O -> F e. ( Base ` P ) ) |
12 |
6 11
|
syl |
|- ( ph -> F e. ( Base ` P ) ) |
13 |
|
eqid |
|- ( 0g ` P ) = ( 0g ` P ) |
14 |
3 13 2
|
mon1pn0 |
|- ( F e. O -> F =/= ( 0g ` P ) ) |
15 |
6 14
|
syl |
|- ( ph -> F =/= ( 0g ` P ) ) |
16 |
1 3 13 10
|
deg1nn0cl |
|- ( ( R e. Ring /\ F e. ( Base ` P ) /\ F =/= ( 0g ` P ) ) -> ( D ` F ) e. NN0 ) |
17 |
5 12 15 16
|
syl3anc |
|- ( ph -> ( D ` F ) e. NN0 ) |
18 |
7 17
|
eqeltrrd |
|- ( ph -> X e. NN0 ) |
19 |
18
|
nn0red |
|- ( ph -> X e. RR ) |
20 |
19
|
leidd |
|- ( ph -> X <_ X ) |
21 |
7 20
|
eqbrtrd |
|- ( ph -> ( D ` F ) <_ X ) |
22 |
3 10 2
|
mon1pcl |
|- ( G e. O -> G e. ( Base ` P ) ) |
23 |
8 22
|
syl |
|- ( ph -> G e. ( Base ` P ) ) |
24 |
9 20
|
eqbrtrd |
|- ( ph -> ( D ` G ) <_ X ) |
25 |
|
eqid |
|- ( coe1 ` F ) = ( coe1 ` F ) |
26 |
|
eqid |
|- ( coe1 ` G ) = ( coe1 ` G ) |
27 |
7
|
fveq2d |
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( ( coe1 ` F ) ` X ) ) |
28 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
29 |
1 28 2
|
mon1pldg |
|- ( F e. O -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( 1r ` R ) ) |
30 |
6 29
|
syl |
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( 1r ` R ) ) |
31 |
27 30
|
eqtr3d |
|- ( ph -> ( ( coe1 ` F ) ` X ) = ( 1r ` R ) ) |
32 |
1 28 2
|
mon1pldg |
|- ( G e. O -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) ) |
33 |
8 32
|
syl |
|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) ) |
34 |
9
|
fveq2d |
|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( ( coe1 ` G ) ` X ) ) |
35 |
31 33 34
|
3eqtr2d |
|- ( ph -> ( ( coe1 ` F ) ` X ) = ( ( coe1 ` G ) ` X ) ) |
36 |
1 3 10 4 18 5 12 21 23 24 25 26 35
|
deg1sublt |
|- ( ph -> ( D ` ( F .- G ) ) < X ) |