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 = ( Poly1 ` R )
	deg1addle.d	|- D = ( deg1 ` R )
	deg1addle.r	|- ( ph -> R e. Ring )
	deg1vscale.b	|- B = ( Base ` Y )
	deg1vscale.k	|- K = ( Base ` R )
	deg1vscale.p	|- .x. = ( .s ` Y )
	deg1vscale.f	|- ( ph -> F e. K )
	deg1vscale.g	|- ( ph -> G e. B )
Assertion	deg1vscale	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	|- Y = ( Poly1 ` R )
2		deg1addle.d	|- D = ( deg1 ` R )
3		deg1addle.r	|- ( ph -> R e. Ring )
4		deg1vscale.b	|- B = ( Base ` Y )
5		deg1vscale.k	|- K = ( Base ` R )
6		deg1vscale.p	|- .x. = ( .s ` Y )
7		deg1vscale.f	|- ( ph -> F e. K )
8		deg1vscale.g	|- ( ph -> G e. B )
9		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
10	2	deg1fval	|- D = ( 1o mDeg R )
11		1on	|- 1o e. On
12	11	a1i	|- ( ph -> 1o e. On )
13		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
14	1 13 4	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
15	1 9 6	ply1vsca	|- .x. = ( .s ` ( 1o mPoly R ) )
16	9 10 12 3 14 5 15 7 8	mdegvscale	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )