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 ) )