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\mathrm{mPoly}R$$
	mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
	mdegaddle.i	$$⊢\phi \to I\in V$$
	mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mdegmulle2.b	$$⊢B={\mathrm{Base}}_Y$$
	mdegmulle2.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	mdegmulle2.f	$$⊢\phi \to F\in B$$
	mdegmulle2.g	$$⊢\phi \to G\in B$$
	mdegmulle2.j1	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	mdegmulle2.k1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	mdegmulle2.j2	$$⊢\phi \to D\left(F\right)\le J$$
	mdegmulle2.k2	$$⊢\phi \to D\left(G\right)\le K$$
Assertion	mdegmulle2	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le J+K$$

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	$$⊢Y=I\mathrm{mPoly}R$$
2		mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
3		mdegaddle.i	$$⊢\phi \to I\in V$$
4		mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mdegmulle2.b	$$⊢B={\mathrm{Base}}_Y$$
6		mdegmulle2.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
7		mdegmulle2.f	$$⊢\phi \to F\in B$$
8		mdegmulle2.g	$$⊢\phi \to G\in B$$
9		mdegmulle2.j1	$$⊢\phi \to J\in {\mathbb{N}}_0$$
10		mdegmulle2.k1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
11		mdegmulle2.j2	$$⊢\phi \to D\left(F\right)\le J$$
12		mdegmulle2.k2	$$⊢\phi \to D\left(G\right)\le K$$
13		eqid	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
14		eqid	$$⊢\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)$$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	mdegmullem	$$⊢\phi \to D\left(F\underset{\dot{}}{·}G\right)\le J+K$$