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 e. _V , r e. _V |-> ( f e. ( Base ` ( i mPoly r ) ) |-> sup ( ran ( h e. ( f supp ( 0g ` r ) ) |-> ( CCfld gsum h ) ) , RR* , < ) ) )
2 1 reldmmpo 
 |-  Rel dom mDeg