Theorem deg1vscale

Description: The degree of a scalar times a polynomial is at most the degree of the original polynomial. (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}$$
	deg1vscale.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1vscale.k	$$⊢K={\mathrm{Base}}_R$$
	deg1vscale.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	deg1vscale.f	$$⊢\phi \to F\in K$$
	deg1vscale.g	$$⊢\phi \to G\in B$$
Assertion	deg1vscale	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le D\left(G\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		deg1vscale.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1vscale.k	$$⊢K={\mathrm{Base}}_R$$
6		deg1vscale.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
7		deg1vscale.f	$$⊢\phi \to F\in K$$
8		deg1vscale.g	$$⊢\phi \to G\in B$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
10	2	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
11		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
12	11	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
13		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
14	1 13 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
15	1 9 6	ply1vsca	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	9 10 12 3 14 5 15 7 8	mdegvscale	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le D\left(G\right)$$