ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reldmprds Unicode version

Theorem reldmprds 12155
Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
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 12154 . 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 ) ) ) ) >. ,  <. ( .i `  ndx ) ,  ( f  e.  v ,  g  e.  v  |->  ( s  gsumg  ( x  e.  dom  r  |->  ( ( f `  x
) ( .i `  ( 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 ) ) ) ) )
>. } ) ) )
21reldmmpo 5882 1  |-  Rel  dom  X_s
Colors of variables: wff set class
Syntax hints:    /\ wa 103   A.wral 2416   _Vcvv 2686   [_csb 3003    u. cun 3069    C_ wss 3071   {csn 3527   {cpr 3528   {ctp 3529   <.cop 3530   class class class wbr 3929   {copab 3988    |-> cmpt 3989    X. cxp 4537   dom cdm 4539   ran crn 4540    o. ccom 4543   Rel wrel 4544   ` cfv 5123  (class class class)co 5774    e. cmpo 5776   1stc1st 6036   2ndc2nd 6037   X_cixp 6592   supcsup 6869   0cc0 7627   RR*cxr 7806    < clt 7807   ndxcnx 11965   Basecbs 11968   +g cplusg 12030   .rcmulr 12031  Scalarcsca 12033   .scvsca 12034   .icip 12035  TopSetcts 12036   lecple 12037   distcds 12039   Hom chom 12041  compcco 12042   TopOpenctopn 12130   Xt_cpt 12145    gsumg cgsu 12147   X_scprds 12152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930  df-opab 3990  df-xp 4545  df-rel 4546  df-dm 4549  df-oprab 5778  df-mpo 5779  df-prds 12154
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator