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

Metamath Proof Explorer

Theorem deg1addle2

Description: If both factors have degree bounded by L , then the sum of the polynomials also has degree bounded by L . (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1addle.y 
|- Y = ( Poly1 ` R )
deg1addle.d 
|- D = ( deg1 ` R )
deg1addle.r 
|- ( ph -> R e. Ring )
deg1addle.b 
|- B = ( Base ` Y )
deg1addle.p 
|- .+ = ( +g ` Y )
deg1addle.f 
|- ( ph -> F e. B )
deg1addle.g 
|- ( ph -> G e. B )
deg1addle2.l1 
|- ( ph -> L e. RR* )
deg1addle2.l2 
|- ( ph -> ( D ` F ) <_ L )
deg1addle2.l3 
|- ( ph -> ( D ` G ) <_ L )
Assertion deg1addle2 
|- ( ph -> ( D ` ( F .+ G ) ) <_ L )

Proof

Step Hyp Ref Expression
1 deg1addle.y 
 |-  Y = ( Poly1 ` R )
2 deg1addle.d 
 |-  D = ( deg1 ` R )
3 deg1addle.r 
 |-  ( ph -> R e. Ring )
4 deg1addle.b 
 |-  B = ( Base ` Y )
5 deg1addle.p 
 |-  .+ = ( +g ` Y )
6 deg1addle.f 
 |-  ( ph -> F e. B )
7 deg1addle.g 
 |-  ( ph -> G e. B )
8 deg1addle2.l1 
 |-  ( ph -> L e. RR* )
9 deg1addle2.l2 
 |-  ( ph -> ( D ` F ) <_ L )
10 deg1addle2.l3 
 |-  ( ph -> ( D ` G ) <_ L )
11 1 ply1ring 
 |-  ( R e. Ring -> Y e. Ring )
12 3 11 syl 
 |-  ( ph -> Y e. Ring )
13 4 5 ringacl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .+ G ) e. B )
14 12 6 7 13 syl3anc 
 |-  ( ph -> ( F .+ G ) e. B )
15 2 1 4 deg1xrcl 
 |-  ( ( F .+ G ) e. B -> ( D ` ( F .+ G ) ) e. RR* )
16 14 15 syl 
 |-  ( ph -> ( D ` ( F .+ G ) ) e. RR* )
17 2 1 4 deg1xrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
18 7 17 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
19 2 1 4 deg1xrcl 
 |-  ( F e. B -> ( D ` F ) e. RR* )
20 6 19 syl 
 |-  ( ph -> ( D ` F ) e. RR* )
21 18 20 ifcld 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) e. RR* )
22 1 2 3 4 5 6 7 deg1addle 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )
23 xrmaxle 
 |-  ( ( ( D ` F ) e. RR* /\ ( D ` G ) e. RR* /\ L e. RR* ) -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L <-> ( ( D ` F ) <_ L /\ ( D ` G ) <_ L ) ) )
24 20 18 8 23 syl3anc 
 |-  ( ph -> ( if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L <-> ( ( D ` F ) <_ L /\ ( D ` G ) <_ L ) ) )
25 9 10 24 mpbir2and 
 |-  ( ph -> if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) <_ L )
26 16 21 8 22 25 xrletrd 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ L )