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

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1vscale.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1vscale.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
6		deg1vscale.p	⊢ · = ( ·𝑠 ‘ 𝑌 )
7		deg1vscale.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
8		deg1vscale.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	mdegvscale	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 · 𝐺 ) ) ≤ ( 𝐷 ‘ 𝐺 ) )