Theorem reldmmdeg

Description: Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	reldmmdeg	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mDeg}$$

Proof

Step	Hyp	Ref	Expression
1		df-mdeg	$$⊢\mathrm{mDeg}=\left(i\in \mathrm{V},r\in \mathrm{V}⟼\left(f\in {\mathrm{Base}}_{\left(i\mathrm{mPoly}r\right)}⟼sup\left(\mathrm{ran}\left(h\in {supp}_{0_r}\left(f\right)⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right),{ℝ}^{*},<\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mDeg}$$