This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Poly}_{1} (R)$
		deg1addle.d	$⊢ D = \deg_{1} (R)$
		deg1addle.r	$⊢ φ \to R \in Ring$
		deg1vsca.b	$⊢ B = {Base}_{Y}$
		deg1vsca.e	$⊢ E = RLReg (R)$
		deg1vsca.p	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
		deg1vsca.f	$⊢ φ \to F \in E$
		deg1vsca.g	$⊢ φ \to G \in B$
	Assertion	deg1vsca	$⊢ φ \to D (F \underset{˙}{\cdot} G) = D (G)$

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	$⊢ Y = {Poly}_{1} (R)$
2		deg1addle.d	$⊢ D = \deg_{1} (R)$
3		deg1addle.r	$⊢ φ \to R \in Ring$
4		deg1vsca.b	$⊢ B = {Base}_{Y}$
5		deg1vsca.e	$⊢ E = RLReg (R)$
6		deg1vsca.p	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
7		deg1vsca.f	$⊢ φ \to F \in E$
8		deg1vsca.g	$⊢ φ \to G \in B$
9		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
10	2	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
11		1on	$⊢ 1_{𝑜} \in On$
12	11	a1i	$⊢ φ \to 1_{𝑜} \in On$
13	1 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
14	1 9 6	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
15	9 10 12 3 13 5 14 7 8	mdegvsca	$⊢ φ \to D (F \underset{˙}{\cdot} G) = D (G)$