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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1vsca.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1vsca.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	deg1vsca.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
	deg1vsca.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
	deg1vsca.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	deg1vsca	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1vsca.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1vsca.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
6		deg1vsca.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
7		deg1vsca.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐸 )
8		deg1vsca.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
9		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
10	2	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
11		1on	⊢ 1o ∈ On
12	11	a1i	⊢ ( 𝜑 → 1o ∈ On )
13		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
14	1 13 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
15	1 9 6	ply1vsca	⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
16	9 10 12 3 14 5 15 7 8	mdegvsca	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )