Theorem deg1vsca

Description: The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-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}$$
	deg1vsca.b	$$⊢B={\mathrm{Base}}_Y$$
	deg1vsca.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	deg1vsca.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	deg1vsca.f	$$⊢\phi \to F\in E$$
	deg1vsca.g	$$⊢\phi \to G\in B$$
Assertion	deg1vsca	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=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		deg1vsca.b	$$⊢B={\mathrm{Base}}_Y$$
5		deg1vsca.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
6		deg1vsca.p	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
7		deg1vsca.f	$$⊢\phi \to F\in E$$
8		deg1vsca.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	mdegvsca	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)=D\left(G\right)$$