This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )