This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = i ∈ V , r ∈ V ⟼ f ∈ Base i mPoly r ⟼ sup ran ⁡ h ∈ supp 0 r⁡ f ⟼ ∑ ℂ fld h ℝ * <
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ mDeg