Description: The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | reldmmpl | |- Rel dom mPoly |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpl | |- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / s ]_ ( s |`s { f e. ( Base ` s ) | f finSupp ( 0g ` r ) } ) ) |
|
2 | 1 | reldmmpo | |- Rel dom mPoly |