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

Theorem reldmpsr 17440
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 17435 . 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 ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( 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 ) } ) ) >. } ) )
21reldmmpt2 6213 1  |-  Rel  dom mPwSer
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   {crab 2731   _Vcvv 2984   [_csb 3300    u. cun 3338   {csn 3889   {ctp 3893   <.cop 3895   class class class wbr 4304    e. cmpt 4362    X. cxp 4850   `'ccnv 4851   dom cdm 4852    |` cres 4854   "cima 4855   Rel wrel 4857   ` cfv 5430  (class class class)co 6103    e. cmpt2 6105    oFcof 6330    oRcofr 6331    ^m cmap 7226   Fincfn 7322    <_ cle 9431    - cmin 9607   NNcn 10334   NN0cn0 10591   ndxcnx 14183   Basecbs 14186   +g cplusg 14250   .rcmulr 14251  Scalarcsca 14253   .scvsca 14254  TopSetcts 14256   TopOpenctopn 14372   Xt_cpt 14389    gsumg cgsu 14391   mPwSer cmps 17430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-xp 4858  df-rel 4859  df-dm 4862  df-oprab 6107  df-mpt2 6108  df-psr 17435
This theorem is referenced by:  psrbas  17460  psrbasOLD  17461  psrelbas  17462  psrplusg  17464  psraddcl  17466  psrmulr  17467  psrmulcllem  17470  psrvscafval  17473  psrvscacl  17476  resspsrbas  17499  resspsradd  17500  resspsrmul  17501  mplval  17513  opsrle  17569  opsrbaslem  17571  psrbaspropd  17701  psropprmul  17705
  Copyright terms: Public domain W3C validator