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