Theorem reldmmdeg

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

	Ref	Expression
Assertion	reldmmdeg	⊢ Rel dom mDeg

Proof

Step	Hyp	Ref	Expression
1		df-mdeg	⊢ mDeg = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ sup ( ran ( ℎ ∈ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ↦ ( ℂfld Σg ℎ ) ) , ℝ* , < ) ) )
2	1	reldmmpo	⊢ Rel dom mDeg