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={\mathrm{Poly}}_1\left(R\right)$$
	deg1addle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1addle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1addle.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1addle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	deg1addle.f	$$⊢\phi \to F\in B$$
	deg1addle.g	$$⊢\phi \to G\in B$$
	deg1addle2.l1	$$⊢\phi \to L\in {ℝ}^{*}$$
	deg1addle2.l2	$$⊢\phi \to D\left(F\right)\le L$$
	deg1addle2.l3	$$⊢\phi \to D\left(G\right)\le L$$
Assertion	deg1addle2	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le L$$

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		deg1addle.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		deg1addle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		deg1addle.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1addle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
6		deg1addle.f	$$⊢\phi \to F\in B$$
7		deg1addle.g	$$⊢\phi \to G\in B$$
8		deg1addle2.l1	$$⊢\phi \to L\in {ℝ}^{*}$$
9		deg1addle2.l2	$$⊢\phi \to D\left(F\right)\le L$$
10		deg1addle2.l3	$$⊢\phi \to D\left(G\right)\le L$$
11	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
12	3 11	syl	$$⊢\phi \to Y\in \mathrm{Ring}$$
13	4 5	ringacl	$$⊢\left(Y\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{+}G\in B$$
14	12 6 7 13	syl3anc	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$
15	2 1 4	deg1xrcl	$$⊢F\underset{\dot{}}{+}G\in B\to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
16	14 15	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\in {ℝ}^{*}$$
17	2 1 4	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
18	7 17	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
19	2 1 4	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
20	6 19	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
21	18 20	ifcld	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}$$
22	1 2 3 4 5 6 7	deg1addle	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
23		xrmaxle	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\wedge L\in {ℝ}^{*}\right)\to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L\leftrightarrow \left(D\left(F\right)\le L\wedge D\left(G\right)\le L\right)\right)$$
24	20 18 8 23	syl3anc	$$⊢\phi \to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L\leftrightarrow \left(D\left(F\right)\le L\wedge D\left(G\right)\le L\right)\right)$$
25	9 10 24	mpbir2and	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L$$
26	16 21 8 22 25	xrletrd	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le L$$