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

Definition df-prds 13364
Description: Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.)
Assertion
Ref Expression
df-prds  |-  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 ) ) ) ) )
>. } ) ) )
Distinct variable group:    a, c, d, e, f, g, h, s, r, x, v

Detailed syntax breakdown of Definition df-prds
StepHypRef Expression
1 cprds 13362 . 2  class  X_s
2 vs . . 3  set  s
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vv . . . 4  set  v
6 vx . . . . 5  set  x
73cv 1631 . . . . . 6  class  r
87cdm 4705 . . . . 5  class  dom  r
96cv 1631 . . . . . . 7  class  x
109, 7cfv 5271 . . . . . 6  class  ( r `
 x )
11 cbs 13164 . . . . . 6  class  Base
1210, 11cfv 5271 . . . . 5  class  ( Base `  ( r `  x
) )
136, 8, 12cixp 6833 . . . 4  class  X_ x  e.  dom  r ( Base `  ( r `  x
) )
14 vh . . . . 5  set  h
15 vf . . . . . 6  set  f
16 vg . . . . . 6  set  g
175cv 1631 . . . . . 6  class  v
1815cv 1631 . . . . . . . . 9  class  f
199, 18cfv 5271 . . . . . . . 8  class  ( f `
 x )
2016cv 1631 . . . . . . . . 9  class  g
219, 20cfv 5271 . . . . . . . 8  class  ( g `
 x )
22 chom 13235 . . . . . . . . 9  class  Hom
2310, 22cfv 5271 . . . . . . . 8  class  (  Hom  `  ( r `  x
) )
2419, 21, 23co 5874 . . . . . . 7  class  ( ( f `  x ) (  Hom  `  (
r `  x )
) ( g `  x ) )
256, 8, 24cixp 6833 . . . . . 6  class  X_ x  e.  dom  r ( ( f `  x ) (  Hom  `  (
r `  x )
) ( g `  x ) )
2615, 16, 17, 17, 25cmpt2 5876 . . . . 5  class  ( f  e.  v ,  g  e.  v  |->  X_ x  e.  dom  r ( ( f `  x ) (  Hom  `  (
r `  x )
) ( g `  x ) ) )
27 cnx 13161 . . . . . . . . . 10  class  ndx
2827, 11cfv 5271 . . . . . . . . 9  class  ( Base `  ndx )
2928, 17cop 3656 . . . . . . . 8  class  <. ( Base `  ndx ) ,  v >.
30 cplusg 13224 . . . . . . . . . 10  class  +g
3127, 30cfv 5271 . . . . . . . . 9  class  ( +g  ` 
ndx )
3210, 30cfv 5271 . . . . . . . . . . . 12  class  ( +g  `  ( r `  x
) )
3319, 21, 32co 5874 . . . . . . . . . . 11  class  ( ( f `  x ) ( +g  `  (
r `  x )
) ( g `  x ) )
346, 8, 33cmpt 4093 . . . . . . . . . 10  class  ( x  e.  dom  r  |->  ( ( f `  x
) ( +g  `  (
r `  x )
) ( g `  x ) ) )
3515, 16, 17, 17, 34cmpt2 5876 . . . . . . . . 9  class  ( f  e.  v ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( ( f `  x
) ( +g  `  (
r `  x )
) ( g `  x ) ) ) )
3631, 35cop 3656 . . . . . . . 8  class  <. ( +g  `  ndx ) ,  ( f  e.  v ,  g  e.  v 
|->  ( x  e.  dom  r  |->  ( ( f `
 x ) ( +g  `  ( r `
 x ) ) ( g `  x
) ) ) )
>.
37 cmulr 13225 . . . . . . . . . 10  class  .r
3827, 37cfv 5271 . . . . . . . . 9  class  ( .r
`  ndx )
3910, 37cfv 5271 . . . . . . . . . . . 12  class  ( .r
`  ( r `  x ) )
4019, 21, 39co 5874 . . . . . . . . . . 11  class  ( ( f `  x ) ( .r `  (
r `  x )
) ( g `  x ) )
416, 8, 40cmpt 4093 . . . . . . . . . 10  class  ( x  e.  dom  r  |->  ( ( f `  x
) ( .r `  ( r `  x
) ) ( g `
 x ) ) )
4215, 16, 17, 17, 41cmpt2 5876 . . . . . . . . 9  class  ( f  e.  v ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( ( f `  x
) ( .r `  ( r `  x
) ) ( g `
 x ) ) ) )
4338, 42cop 3656 . . . . . . . 8  class  <. ( .r `  ndx ) ,  ( f  e.  v ,  g  e.  v 
|->  ( x  e.  dom  r  |->  ( ( f `
 x ) ( .r `  ( r `
 x ) ) ( g `  x
) ) ) )
>.
4429, 36, 43ctp 3655 . . . . . . 7  class  { <. (
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 ) ) ) ) >. }
45 csca 13227 . . . . . . . . . 10  class Scalar
4627, 45cfv 5271 . . . . . . . . 9  class  (Scalar `  ndx )
472cv 1631 . . . . . . . . 9  class  s
4846, 47cop 3656 . . . . . . . 8  class  <. (Scalar ` 
ndx ) ,  s
>.
49 cvsca 13228 . . . . . . . . . 10  class  .s
5027, 49cfv 5271 . . . . . . . . 9  class  ( .s
`  ndx )
5147, 11cfv 5271 . . . . . . . . . 10  class  ( Base `  s )
5210, 49cfv 5271 . . . . . . . . . . . 12  class  ( .s
`  ( r `  x ) )
5318, 21, 52co 5874 . . . . . . . . . . 11  class  ( f ( .s `  (
r `  x )
) ( g `  x ) )
546, 8, 53cmpt 4093 . . . . . . . . . 10  class  ( x  e.  dom  r  |->  ( f ( .s `  ( r `  x
) ) ( g `
 x ) ) )
5515, 16, 51, 17, 54cmpt2 5876 . . . . . . . . 9  class  ( f  e.  ( Base `  s
) ,  g  e.  v  |->  ( x  e. 
dom  r  |->  ( f ( .s `  (
r `  x )
) ( g `  x ) ) ) )
5650, 55cop 3656 . . . . . . . 8  class  <. ( .s `  ndx ) ,  ( f  e.  (
Base `  s ) ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( f ( .s `  ( r `
 x ) ) ( g `  x
) ) ) )
>.
5748, 56cpr 3654 . . . . . . 7  class  { <. (Scalar `  ndx ) ,  s
>. ,  <. ( .s
`  ndx ) ,  ( f  e.  ( Base `  s ) ,  g  e.  v  |->  ( x  e.  dom  r  |->  ( f ( .s `  ( r `  x
) ) ( g `
 x ) ) ) ) >. }
5844, 57cun 3163 . . . . . 6  class  ( {
<. ( 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 ) ) ) ) >. } )
59 cts 13230 . . . . . . . . . 10  class TopSet
6027, 59cfv 5271 . . . . . . . . 9  class  (TopSet `  ndx )
61 ctopn 13342 . . . . . . . . . . 11  class  TopOpen
6261, 7ccom 4709 . . . . . . . . . 10  class  ( TopOpen  o.  r )
63 cpt 13359 . . . . . . . . . 10  class  Xt_
6462, 63cfv 5271 . . . . . . . . 9  class  ( Xt_ `  ( TopOpen  o.  r )
)
6560, 64cop 3656 . . . . . . . 8  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( TopOpen  o.  r
) ) >.
66 cple 13231 . . . . . . . . . 10  class  le
6727, 66cfv 5271 . . . . . . . . 9  class  ( le
`  ndx )
6818, 20cpr 3654 . . . . . . . . . . . 12  class  { f ,  g }
6968, 17wss 3165 . . . . . . . . . . 11  wff  { f ,  g }  C_  v
7010, 66cfv 5271 . . . . . . . . . . . . 13  class  ( le
`  ( r `  x ) )
7119, 21, 70wbr 4039 . . . . . . . . . . . 12  wff  ( f `
 x ) ( le `  ( r `
 x ) ) ( g `  x
)
7271, 6, 8wral 2556 . . . . . . . . . . 11  wff  A. x  e.  dom  r ( f `
 x ) ( le `  ( r `
 x ) ) ( g `  x
)
7369, 72wa 358 . . . . . . . . . 10  wff  ( { f ,  g } 
C_  v  /\  A. x  e.  dom  r ( f `  x ) ( le `  (
r `  x )
) ( g `  x ) )
7473, 15, 16copab 4092 . . . . . . . . 9  class  { <. f ,  g >.  |  ( { f ,  g }  C_  v  /\  A. x  e.  dom  r
( f `  x
) ( le `  ( r `  x
) ) ( g `
 x ) ) }
7567, 74cop 3656 . . . . . . . 8  class  <. ( le `  ndx ) ,  { <. f ,  g
>.  |  ( {
f ,  g } 
C_  v  /\  A. x  e.  dom  r ( f `  x ) ( le `  (
r `  x )
) ( g `  x ) ) }
>.
76 cds 13233 . . . . . . . . . 10  class  dist
7727, 76cfv 5271 . . . . . . . . 9  class  ( dist `  ndx )
7810, 76cfv 5271 . . . . . . . . . . . . . . 15  class  ( dist `  ( r `  x
) )
7919, 21, 78co 5874 . . . . . . . . . . . . . 14  class  ( ( f `  x ) ( dist `  (
r `  x )
) ( g `  x ) )
806, 8, 79cmpt 4093 . . . . . . . . . . . . 13  class  ( x  e.  dom  r  |->  ( ( f `  x
) ( dist `  (
r `  x )
) ( g `  x ) ) )
8180crn 4706 . . . . . . . . . . . 12  class  ran  (
x  e.  dom  r  |->  ( ( f `  x ) ( dist `  ( r `  x
) ) ( g `
 x ) ) )
82 cc0 8753 . . . . . . . . . . . . 13  class  0
8382csn 3653 . . . . . . . . . . . 12  class  { 0 }
8481, 83cun 3163 . . . . . . . . . . 11  class  ( ran  ( x  e.  dom  r  |->  ( ( f `
 x ) (
dist `  ( r `  x ) ) ( g `  x ) ) )  u.  {
0 } )
85 cxr 8882 . . . . . . . . . . 11  class  RR*
86 clt 8883 . . . . . . . . . . 11  class  <
8784, 85, 86csup 7209 . . . . . . . . . 10  class  sup (
( ran  ( x  e.  dom  r  |->  ( ( f `  x ) ( dist `  (
r `  x )
) ( g `  x ) ) )  u.  { 0 } ) ,  RR* ,  <  )
8815, 16, 17, 17, 87cmpt2 5876 . . . . . . . . 9  class  ( f  e.  v ,  g  e.  v  |->  sup (
( ran  ( x  e.  dom  r  |->  ( ( f `  x ) ( dist `  (
r `  x )
) ( g `  x ) ) )  u.  { 0 } ) ,  RR* ,  <  ) )
8977, 88cop 3656 . . . . . . . 8  class  <. ( dist `  ndx ) ,  ( f  e.  v ,  g  e.  v 
|->  sup ( ( ran  ( x  e.  dom  r  |->  ( ( f `
 x ) (
dist `  ( r `  x ) ) ( g `  x ) ) )  u.  {
0 } ) , 
RR* ,  <  ) )
>.
9065, 75, 89ctp 3655 . . . . . . 7  class  { <. (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* ,  <  ) ) >. }
9127, 22cfv 5271 . . . . . . . . 9  class  (  Hom  `  ndx )
9214cv 1631 . . . . . . . . 9  class  h
9391, 92cop 3656 . . . . . . . 8  class  <. (  Hom  `  ndx ) ,  h >.
94 cco 13236 . . . . . . . . . 10  class comp
9527, 94cfv 5271 . . . . . . . . 9  class  (comp `  ndx )
96 va . . . . . . . . . 10  set  a
97 vc . . . . . . . . . 10  set  c
9817, 17cxp 4703 . . . . . . . . . 10  class  ( v  X.  v )
99 vd . . . . . . . . . . 11  set  d
100 ve . . . . . . . . . . 11  set  e
10197cv 1631 . . . . . . . . . . . 12  class  c
10296cv 1631 . . . . . . . . . . . . 13  class  a
103 c2nd 6137 . . . . . . . . . . . . 13  class  2nd
104102, 103cfv 5271 . . . . . . . . . . . 12  class  ( 2nd `  a )
105101, 104, 92co 5874 . . . . . . . . . . 11  class  ( c h ( 2nd `  a
) )
106102, 92cfv 5271 . . . . . . . . . . 11  class  ( h `
 a )
10799cv 1631 . . . . . . . . . . . . . 14  class  d
1089, 107cfv 5271 . . . . . . . . . . . . 13  class  ( d `
 x )
109100cv 1631 . . . . . . . . . . . . . 14  class  e
1109, 109cfv 5271 . . . . . . . . . . . . 13  class  ( e `
 x )
111 c1st 6136 . . . . . . . . . . . . . . . . 17  class  1st
112102, 111cfv 5271 . . . . . . . . . . . . . . . 16  class  ( 1st `  a )
1139, 112cfv 5271 . . . . . . . . . . . . . . 15  class  ( ( 1st `  a ) `
 x )
1149, 104cfv 5271 . . . . . . . . . . . . . . 15  class  ( ( 2nd `  a ) `
 x )
115113, 114cop 3656 . . . . . . . . . . . . . 14  class  <. (
( 1st `  a
) `  x ) ,  ( ( 2nd `  a ) `  x
) >.
1169, 101cfv 5271 . . . . . . . . . . . . . 14  class  ( c `
 x )
11710, 94cfv 5271 . . . . . . . . . . . . . 14  class  (comp `  ( r `  x
) )
118115, 116, 117co 5874 . . . . . . . . . . . . 13  class  ( <.
( ( 1st `  a
) `  x ) ,  ( ( 2nd `  a ) `  x
) >. (comp `  (
r `  x )
) ( c `  x ) )
119108, 110, 118co 5874 . . . . . . . . . . . 12  class  ( ( d `  x ) ( <. ( ( 1st `  a ) `  x
) ,  ( ( 2nd `  a ) `
 x ) >.
(comp `  ( r `  x ) ) ( c `  x ) ) ( e `  x ) )
1206, 8, 119cmpt 4093 . . . . . . . . . . 11  class  ( x  e.  dom  r  |->  ( ( d `  x
) ( <. (
( 1st `  a
) `  x ) ,  ( ( 2nd `  a ) `  x
) >. (comp `  (
r `  x )
) ( c `  x ) ) ( e `  x ) ) )
12199, 100, 105, 106, 120cmpt2 5876 . . . . . . . . . 10  class  ( 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 ) ) ) )
12296, 97, 98, 17, 121cmpt2 5876 . . . . . . . . 9  class  ( 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 ) ) ) ) )
12395, 122cop 3656 . . . . . . . 8  class  <. (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 ) ) ) ) )
>.
12493, 123cpr 3654 . . . . . . 7  class  { <. (  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 ) ) ) ) )
>. }
12590, 124cun 3163 . . . . . 6  class  ( {
<. (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 ) ) ) ) )
>. } )
12658, 125cun 3163 . . . . 5  class  ( ( { <. ( 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 ) ) ) ) )
>. } ) )
12714, 26, 126csb 3094 . . . 4  class  [_ (
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 ) ) ) ) )
>. } ) )
1285, 13, 127csb 3094 . . 3  class  [_ 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 ) ) ) ) )
>. } ) )
1292, 3, 4, 4, 128cmpt2 5876 . 2  class  ( 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 ) ) ) ) )
>. } ) ) )
1301, 129wceq 1632 1  wff  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 ) ) ) ) )
>. } ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldmprds  13365  prdsval  13371
  Copyright terms: Public domain W3C validator