Theorem deg1mulle2

Description: Produce a bound on the product of two univariate polynomials given bounds on 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}$$
	deg1mulle2.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1mulle2.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	deg1mulle2.f	$$⊢\phi \to F\in B$$
	deg1mulle2.g	$$⊢\phi \to G\in B$$
	deg1mulle2.j1	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	deg1mulle2.k1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	deg1mulle2.j2	$$⊢\phi \to D\left(F\right)\le J$$
	deg1mulle2.k2	$$⊢\phi \to D\left(G\right)\le K$$
Assertion	deg1mulle2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le J+K$$

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		deg1mulle2.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1mulle2.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
6		deg1mulle2.f	$$⊢\phi \to F\in B$$
7		deg1mulle2.g	$$⊢\phi \to G\in B$$
8		deg1mulle2.j1	$$⊢\phi \to J\in {\mathbb{N}}_0$$
9		deg1mulle2.k1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
10		deg1mulle2.j2	$$⊢\phi \to D\left(F\right)\le J$$
11		deg1mulle2.k2	$$⊢\phi \to D\left(G\right)\le K$$
12		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
13	2	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
14		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
15	14	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
16		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
17	1 16 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	1 12 5	ply1mulr	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	12 13 15 3 17 18 6 7 8 9 10 11	mdegmulle2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le J+K$$