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 )

Metamath Proof Explorer

Theorem deg1addle2

Proof