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

Metamath Proof Explorer

Theorem reldmpsr

Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion reldmpsr 
|- Rel dom mPwSer

Proof

Step Hyp Ref Expression
1 df-psr 
 |-  mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
2 1 reldmmpo 
 |-  Rel dom mPwSer