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={\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$$
Assertion	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)$$

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		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
9	2	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11	10	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
13	1 8 5	ply1plusg	$$⊢\underset{\dot{}}{+}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
14	1 4	ply1bascl2	$$⊢F\in B\to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
15	6 14	syl	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	1 4	ply1bascl2	$$⊢G\in B\to G\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17	7 16	syl	$$⊢\phi \to G\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	8 9 11 3 12 13 15 17	mdegaddle	$$⊢\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)$$