Theorem deg1mulle2

Description: Produce a bound on the product of two univariate polynomials given bounds on the factors. (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 )
	deg1mulle2.b	|- B = ( Base ` Y )
	deg1mulle2.t	|- .x. = ( .r ` Y )
	deg1mulle2.f	|- ( ph -> F e. B )
	deg1mulle2.g	|- ( ph -> G e. B )
	deg1mulle2.j1	|- ( ph -> J e. NN0 )
	deg1mulle2.k1	|- ( ph -> K e. NN0 )
	deg1mulle2.j2	|- ( ph -> ( D ` F ) <_ J )
	deg1mulle2.k2	|- ( ph -> ( D ` G ) <_ K )
Assertion	deg1mulle2	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )

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		deg1mulle2.b	|- B = ( Base ` Y )
5		deg1mulle2.t	|- .x. = ( .r ` Y )
6		deg1mulle2.f	|- ( ph -> F e. B )
7		deg1mulle2.g	|- ( ph -> G e. B )
8		deg1mulle2.j1	|- ( ph -> J e. NN0 )
9		deg1mulle2.k1	|- ( ph -> K e. NN0 )
10		deg1mulle2.j2	|- ( ph -> ( D ` F ) <_ J )
11		deg1mulle2.k2	|- ( ph -> ( D ` G ) <_ K )
12		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
13	2	deg1fval	|- D = ( 1o mDeg R )
14		1on	|- 1o e. On
15	14	a1i	|- ( ph -> 1o e. On )
16		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
17	1 16 4	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
18	1 12 5	ply1mulr	|- .x. = ( .r ` ( 1o mPoly R ) )
19	12 13 15 3 17 18 6 7 8 9 10 11	mdegmulle2	|- ( ph -> ( D ` ( F .x. G ) ) <_ ( J + K ) )