Theorem mdegmulle2

Description: The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	mdegaddle.y	|- Y = ( I mPoly R )
	mdegaddle.d	|- D = ( I mDeg R )
	mdegaddle.i	|- ( ph -> I e. V )
	mdegaddle.r	|- ( ph -> R e. Ring )
	mdegmulle2.b	|- B = ( Base ` Y )
	mdegmulle2.t	|- .x. = ( .r ` Y )
	mdegmulle2.f	|- ( ph -> F e. B )
	mdegmulle2.g	|- ( ph -> G e. B )
	mdegmulle2.j1	|- ( ph -> J e. NN0 )
	mdegmulle2.k1	|- ( ph -> K e. NN0 )
	mdegmulle2.j2	|- ( ph -> ( D ` F ) <_ J )
	mdegmulle2.k2	|- ( ph -> ( D ` G ) <_ K )
Assertion	mdegmulle2	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	|- Y = ( I mPoly R )
2		mdegaddle.d	|- D = ( I mDeg R )
3		mdegaddle.i	|- ( ph -> I e. V )
4		mdegaddle.r	|- ( ph -> R e. Ring )
5		mdegmulle2.b	|- B = ( Base ` Y )
6		mdegmulle2.t	|- .x. = ( .r ` Y )
7		mdegmulle2.f	|- ( ph -> F e. B )
8		mdegmulle2.g	|- ( ph -> G e. B )
9		mdegmulle2.j1	|- ( ph -> J e. NN0 )
10		mdegmulle2.k1	|- ( ph -> K e. NN0 )
11		mdegmulle2.j2	|- ( ph -> ( D ` F ) <_ J )
12		mdegmulle2.k2	|- ( ph -> ( D ` G ) <_ K )
13		eqid	|- { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
14		eqid	|- ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) )
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mdegmullem	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )