Metamath Proof Explorer


Theorem deg1submon1p

Description: The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses deg1submon1p.d
|- D = ( deg1 ` R )
deg1submon1p.o
|- O = ( Monic1p ` R )
deg1submon1p.p
|- P = ( Poly1 ` R )
deg1submon1p.m
|- .- = ( -g ` P )
deg1submon1p.r
|- ( ph -> R e. Ring )
deg1submon1p.f1
|- ( ph -> F e. O )
deg1submon1p.f2
|- ( ph -> ( D ` F ) = X )
deg1submon1p.g1
|- ( ph -> G e. O )
deg1submon1p.g2
|- ( ph -> ( D ` G ) = X )
Assertion deg1submon1p
|- ( ph -> ( D ` ( F .- G ) ) < X )

Proof

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 )