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

Theorem reldmprds 13365
Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.)
Assertion
Ref Expression
reldmprds  |-  Rel  dom  X_s

Proof of Theorem reldmprds
Dummy variables  a 
c  d  e  f  g  h  s  r  x  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-prds 13364 . 2  |-  X_s  =  (
s  e.  _V , 
r  e.  _V  |->  [_ X_ x  e.  dom  r
( Base `  ( r `  x ) )  / 
v ]_ [_ ( f  e.  v ,  g  e.  v  |->  X_ x  e.  dom  r ( ( f `  x ) (  Hom  `  (
r `  x )
) ( g `  x ) ) )  /  h ]_ (
( { <. ( Base `  ndx ) ,  v >. ,  <. ( +g  `  ndx ) ,  ( f  e.  v ,  g  e.  v 
|->  ( x  e.  dom  r  |->  ( ( f `
 x ) ( +g  `  ( r `
 x ) ) ( g `  x
) ) ) )
>. ,  <. ( .r
`  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( ( f `  x ) ( .r
`  ( r `  x ) ) ( g `  x ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  s
>. ,  <. ( .s
`  ndx ) ,  ( f  e.  ( Base `  s ) ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( f ( .s `  ( r `  x
) ) ( g `
 x ) ) ) ) >. } )  u.  ( { <. (TopSet `  ndx ) ,  (
Xt_ `  ( TopOpen  o.  r
) ) >. ,  <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  v  /\  A. x  e.  dom  r ( f `  x ) ( le `  (
r `  x )
) ( g `  x ) ) }
>. ,  <. ( dist `  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  sup ( ( ran  (
x  e.  dom  r  |->  ( ( f `  x ) ( dist `  ( r `  x
) ) ( g `
 x ) ) )  u.  { 0 } ) ,  RR* ,  <  ) ) >. }  u.  { <. (  Hom  `  ndx ) ,  h >. ,  <. (comp ` 
ndx ) ,  ( a  e.  ( v  X.  v ) ,  c  e.  v  |->  ( d  e.  ( c h ( 2nd `  a
) ) ,  e  e.  ( h `  a )  |->  ( x  e.  dom  r  |->  ( ( d `  x
) ( <. (
( 1st `  a
) `  x ) ,  ( ( 2nd `  a ) `  x
) >. (comp `  (
r `  x )
) ( c `  x ) ) ( e `  x ) ) ) ) )
>. } ) ) )
21reldmmpt2 5971 1  |-  Rel  dom  X_s
Colors of variables: wff set class
Syntax hints:    /\ wa 358   A.wral 2556   _Vcvv 2801   [_csb 3094    u. cun 3163    C_ wss 3165   {csn 3653   {cpr 3654   {ctp 3655   <.cop 3656   class class class wbr 4039   {copab 4092    e. cmpt 4093    X. cxp 4703   dom cdm 4705   ran crn 4706    o. ccom 4709   Rel wrel 4710   ` cfv 5271  (class class class)co 5874    e. cmpt2 5876   1stc1st 6136   2ndc2nd 6137   X_cixp 6833   supcsup 7209   0cc0 8753   RR*cxr 8882    < clt 8883   ndxcnx 13161   Basecbs 13164   +g cplusg 13224   .rcmulr 13225  Scalarcsca 13227   .scvsca 13228  TopSetcts 13230   lecple 13231   distcds 13233    Hom chom 13235  compcco 13236   TopOpenctopn 13342   Xt_cpt 13359   X_scprds 13362
This theorem is referenced by:  dsmmval  27303  dsmmval2  27305  dsmmbas2  27306  dsmmfi  27307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-rel 4712  df-dm 4715  df-oprab 5878  df-mpt2 5879  df-prds 13364
  Copyright terms: Public domain W3C validator