MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmpsr Unicode version

Theorem reldmpsr 16355
Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
reldmpsr  |-  Rel  dom mPwSer

Proof of Theorem reldmpsr
Dummy variables  h  i  r  y  b 
d  f  g  k  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-psr 16344 . 2  |- 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 ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } ) )
21reldmmpt2 6120 1  |-  Rel  dom mPwSer
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   {crab 2653   _Vcvv 2899   [_csb 3194    u. cun 3261   {csn 3757   {ctp 3759   <.cop 3760   class class class wbr 4153    e. cmpt 4207    X. cxp 4816   `'ccnv 4817   dom cdm 4818    |` cres 4820   "cima 4821   Rel wrel 4823   ` cfv 5394  (class class class)co 6020    e. cmpt2 6022    o Fcof 6242    o Rcofr 6243    ^m cmap 6954   Fincfn 7045    <_ cle 9054    - cmin 9223   NNcn 9932   NN0cn0 10153   ndxcnx 13393   Basecbs 13396   +g cplusg 13456   .rcmulr 13457  Scalarcsca 13459   .scvsca 13460  TopSetcts 13462   TopOpenctopn 13576   Xt_cpt 13593    gsumg cgsu 13651   mPwSer cmps 16333
This theorem is referenced by:  psrbas  16370  psrelbas  16371  psrplusg  16372  psraddcl  16374  psrmulr  16375  psrmulcllem  16378  psrvscafval  16381  psrvscacl  16384  resspsrbas  16405  resspsradd  16406  resspsrmul  16407  mplval  16419  opsrle  16463  opsrbaslem  16465  psrbaspropd  16555  psropprmul  16559
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-dm 4828  df-oprab 6024  df-mpt2 6025  df-psr 16344
  Copyright terms: Public domain W3C validator