Metamath Proof Explorer


Theorem r1pdeglt

Description: The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses r1pval.e
|- E = ( rem1p ` R )
r1pval.p
|- P = ( Poly1 ` R )
r1pval.b
|- B = ( Base ` P )
r1pcl.c
|- C = ( Unic1p ` R )
r1pdeglt.d
|- D = ( deg1 ` R )
Assertion r1pdeglt
|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F E G ) ) < ( D ` G ) )

Proof

Step Hyp Ref Expression
1 r1pval.e
 |-  E = ( rem1p ` R )
2 r1pval.p
 |-  P = ( Poly1 ` R )
3 r1pval.b
 |-  B = ( Base ` P )
4 r1pcl.c
 |-  C = ( Unic1p ` R )
5 r1pdeglt.d
 |-  D = ( deg1 ` R )
6 simp2
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> F e. B )
7 2 3 4 uc1pcl
 |-  ( G e. C -> G e. B )
8 7 3ad2ant3
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
9 eqid
 |-  ( quot1p ` R ) = ( quot1p ` R )
10 eqid
 |-  ( .r ` P ) = ( .r ` P )
11 eqid
 |-  ( -g ` P ) = ( -g ` P )
12 1 2 3 9 10 11 r1pval
 |-  ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
13 6 8 12 syl2anc
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
14 13 fveq2d
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F E G ) ) = ( D ` ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ) )
15 eqid
 |-  ( F ( quot1p ` R ) G ) = ( F ( quot1p ` R ) G )
16 9 2 3 5 11 10 4 q1peqb
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( ( F ( quot1p ` R ) G ) e. B /\ ( D ` ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ) < ( D ` G ) ) <-> ( F ( quot1p ` R ) G ) = ( F ( quot1p ` R ) G ) ) )
17 15 16 mpbiri
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F ( quot1p ` R ) G ) e. B /\ ( D ` ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ) < ( D ` G ) ) )
18 17 simprd
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ) < ( D ` G ) )
19 14 18 eqbrtrd
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( D ` ( F E G ) ) < ( D ` G ) )