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

Metamath Proof Explorer

Theorem deg1addle

Description: The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-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 )
Assertion deg1addle 
|- ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )

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 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
9 2 deg1fval 
 |-  D = ( 1o mDeg R )
10 1on 
 |-  1o e. On
11 10 a1i 
 |-  ( ph -> 1o e. On )
12 eqid 
 |-  ( Base ` ( 1o mPoly R ) ) = ( Base ` ( 1o mPoly R ) )
13 1 8 5 ply1plusg 
 |-  .+ = ( +g ` ( 1o mPoly R ) )
14 1 4 ply1bascl2 
 |-  ( F e. B -> F e. ( Base ` ( 1o mPoly R ) ) )
15 6 14 syl 
 |-  ( ph -> F e. ( Base ` ( 1o mPoly R ) ) )
16 1 4 ply1bascl2 
 |-  ( G e. B -> G e. ( Base ` ( 1o mPoly R ) ) )
17 7 16 syl 
 |-  ( ph -> G e. ( Base ` ( 1o mPoly R ) ) )
18 8 9 11 3 12 13 15 17 mdegaddle 
 |-  ( ph -> ( D ` ( F .+ G ) ) <_ if ( ( D ` F ) <_ ( D ` G ) , ( D ` G ) , ( D ` F ) ) )