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

Definition df-imas 13411
Description: Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly  f must either be injective or satisfy the well-definedness condition  f ( a )  =  f ( c )  /\  f ( b )  =  f ( d )  ->  f (
a  +  b )  =  f ( c  +  d ) for each relevant operation.

Note that although we call this an "image" by association to df-ima 4702, in order to keep the definition simple we consider only the case when the domain of  F is equal to the base set of  R. Other cases can be achieved by restricting 
F (with df-res 4701) and/or  R ( with df-ress 13155) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.)

Assertion
Ref Expression
df-imas  |-  "s  =  (
f  e.  _V , 
r  e.  _V  |->  [_ ( Base `  r )  /  v ]_ (
( { <. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >. ,  <. ( .r `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } ) )
Distinct variable group:    f, g, h, i, n, p, q, r, v, x, y

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 13407 . 2  class  "s
2 vf . . 3  set  f
3 vr . . 3  set  r
4 cvv 2788 . . 3  class  _V
5 vv . . . 4  set  v
63cv 1622 . . . . 5  class  r
7 cbs 13148 . . . . 5  class  Base
86, 7cfv 5255 . . . 4  class  ( Base `  r )
9 cnx 13145 . . . . . . . . 9  class  ndx
109, 7cfv 5255 . . . . . . . 8  class  ( Base `  ndx )
112cv 1622 . . . . . . . . 9  class  f
1211crn 4690 . . . . . . . 8  class  ran  f
1310, 12cop 3643 . . . . . . 7  class  <. ( Base `  ndx ) ,  ran  f >.
14 cplusg 13208 . . . . . . . . 9  class  +g
159, 14cfv 5255 . . . . . . . 8  class  ( +g  ` 
ndx )
16 vp . . . . . . . . 9  set  p
175cv 1622 . . . . . . . . 9  class  v
18 vq . . . . . . . . . 10  set  q
1916cv 1622 . . . . . . . . . . . . . 14  class  p
2019, 11cfv 5255 . . . . . . . . . . . . 13  class  ( f `
 p )
2118cv 1622 . . . . . . . . . . . . . 14  class  q
2221, 11cfv 5255 . . . . . . . . . . . . 13  class  ( f `
 q )
2320, 22cop 3643 . . . . . . . . . . . 12  class  <. (
f `  p ) ,  ( f `  q ) >.
246, 14cfv 5255 . . . . . . . . . . . . . 14  class  ( +g  `  r )
2519, 21, 24co 5858 . . . . . . . . . . . . 13  class  ( p ( +g  `  r
) q )
2625, 11cfv 5255 . . . . . . . . . . . 12  class  ( f `
 ( p ( +g  `  r ) q ) )
2723, 26cop 3643 . . . . . . . . . . 11  class  <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>.
2827csn 3640 . . . . . . . . . 10  class  { <. <.
( f `  p
) ,  ( f `
 q ) >. ,  ( f `  ( p ( +g  `  r ) q ) ) >. }
2918, 17, 28ciun 3905 . . . . . . . . 9  class  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. }
3016, 17, 29ciun 3905 . . . . . . . 8  class  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. }
3115, 30cop 3643 . . . . . . 7  class  <. ( +g  `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >.
32 cmulr 13209 . . . . . . . . 9  class  .r
339, 32cfv 5255 . . . . . . . 8  class  ( .r
`  ndx )
346, 32cfv 5255 . . . . . . . . . . . . . 14  class  ( .r
`  r )
3519, 21, 34co 5858 . . . . . . . . . . . . 13  class  ( p ( .r `  r
) q )
3635, 11cfv 5255 . . . . . . . . . . . 12  class  ( f `
 ( p ( .r `  r ) q ) )
3723, 36cop 3643 . . . . . . . . . . 11  class  <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>.
3837csn 3640 . . . . . . . . . 10  class  { <. <.
( f `  p
) ,  ( f `
 q ) >. ,  ( f `  ( p ( .r
`  r ) q ) ) >. }
3918, 17, 38ciun 3905 . . . . . . . . 9  class  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>. }
4016, 17, 39ciun 3905 . . . . . . . 8  class  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>. }
4133, 40cop 3643 . . . . . . 7  class  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >.
4213, 31, 41ctp 3642 . . . . . 6  class  { <. (
Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >. ,  <. ( .r `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }
43 csca 13211 . . . . . . . . 9  class Scalar
449, 43cfv 5255 . . . . . . . 8  class  (Scalar `  ndx )
456, 43cfv 5255 . . . . . . . 8  class  (Scalar `  r )
4644, 45cop 3643 . . . . . . 7  class  <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >.
47 cvsca 13212 . . . . . . . . 9  class  .s
489, 47cfv 5255 . . . . . . . 8  class  ( .s
`  ndx )
49 vx . . . . . . . . . 10  set  x
5045, 7cfv 5255 . . . . . . . . . 10  class  ( Base `  (Scalar `  r )
)
5122csn 3640 . . . . . . . . . 10  class  { ( f `  q ) }
526, 47cfv 5255 . . . . . . . . . . . 12  class  ( .s
`  r )
5319, 21, 52co 5858 . . . . . . . . . . 11  class  ( p ( .s `  r
) q )
5453, 11cfv 5255 . . . . . . . . . 10  class  ( f `
 ( p ( .s `  r ) q ) )
5516, 49, 50, 51, 54cmpt2 5860 . . . . . . . . 9  class  ( p  e.  ( Base `  (Scalar `  r ) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s
`  r ) q ) ) )
5618, 17, 55ciun 3905 . . . . . . . 8  class  U_ q  e.  v  ( p  e.  ( Base `  (Scalar `  r ) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s
`  r ) q ) ) )
5748, 56cop 3643 . . . . . . 7  class  <. ( .s `  ndx ) , 
U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >.
5846, 57cpr 3641 . . . . . 6  class  { <. (Scalar `  ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. }
5942, 58cun 3150 . . . . 5  class  ( {
<. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. } >. ,  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )
60 cts 13214 . . . . . . . 8  class TopSet
619, 60cfv 5255 . . . . . . 7  class  (TopSet `  ndx )
62 ctopn 13326 . . . . . . . . 9  class  TopOpen
636, 62cfv 5255 . . . . . . . 8  class  ( TopOpen `  r )
64 cqtop 13406 . . . . . . . 8  class qTop
6563, 11, 64co 5858 . . . . . . 7  class  ( (
TopOpen `  r ) qTop  f
)
6661, 65cop 3643 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  ( ( TopOpen `  r ) qTop  f ) >.
67 cple 13215 . . . . . . . 8  class  le
689, 67cfv 5255 . . . . . . 7  class  ( le
`  ndx )
696, 67cfv 5255 . . . . . . . . 9  class  ( le
`  r )
7011, 69ccom 4693 . . . . . . . 8  class  ( f  o.  ( le `  r ) )
7111ccnv 4688 . . . . . . . 8  class  `' f
7270, 71ccom 4693 . . . . . . 7  class  ( ( f  o.  ( le
`  r ) )  o.  `' f )
7368, 72cop 3643 . . . . . 6  class  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >.
74 cds 13217 . . . . . . . 8  class  dist
759, 74cfv 5255 . . . . . . 7  class  ( dist `  ndx )
76 vy . . . . . . . 8  set  y
77 vn . . . . . . . . . 10  set  n
78 cn 9746 . . . . . . . . . 10  class  NN
79 vg . . . . . . . . . . . 12  set  g
80 c1 8738 . . . . . . . . . . . . . . . . . 18  class  1
81 vh . . . . . . . . . . . . . . . . . . 19  set  h
8281cv 1622 . . . . . . . . . . . . . . . . . 18  class  h
8380, 82cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( h `
 1 )
84 c1st 6120 . . . . . . . . . . . . . . . . 17  class  1st
8583, 84cfv 5255 . . . . . . . . . . . . . . . 16  class  ( 1st `  ( h `  1
) )
8685, 11cfv 5255 . . . . . . . . . . . . . . 15  class  ( f `
 ( 1st `  (
h `  1 )
) )
8749cv 1622 . . . . . . . . . . . . . . 15  class  x
8886, 87wceq 1623 . . . . . . . . . . . . . 14  wff  ( f `
 ( 1st `  (
h `  1 )
) )  =  x
8977cv 1622 . . . . . . . . . . . . . . . . . 18  class  n
9089, 82cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( h `
 n )
91 c2nd 6121 . . . . . . . . . . . . . . . . 17  class  2nd
9290, 91cfv 5255 . . . . . . . . . . . . . . . 16  class  ( 2nd `  ( h `  n
) )
9392, 11cfv 5255 . . . . . . . . . . . . . . 15  class  ( f `
 ( 2nd `  (
h `  n )
) )
9476cv 1622 . . . . . . . . . . . . . . 15  class  y
9593, 94wceq 1623 . . . . . . . . . . . . . 14  wff  ( f `
 ( 2nd `  (
h `  n )
) )  =  y
96 vi . . . . . . . . . . . . . . . . . . . 20  set  i
9796cv 1622 . . . . . . . . . . . . . . . . . . 19  class  i
9897, 82cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( h `
 i )
9998, 91cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( 2nd `  ( h `  i
) )
10099, 11cfv 5255 . . . . . . . . . . . . . . . 16  class  ( f `
 ( 2nd `  (
h `  i )
) )
101 caddc 8740 . . . . . . . . . . . . . . . . . . . 20  class  +
10297, 80, 101co 5858 . . . . . . . . . . . . . . . . . . 19  class  ( i  +  1 )
103102, 82cfv 5255 . . . . . . . . . . . . . . . . . 18  class  ( h `
 ( i  +  1 ) )
104103, 84cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( 1st `  ( h `  (
i  +  1 ) ) )
105104, 11cfv 5255 . . . . . . . . . . . . . . . 16  class  ( f `
 ( 1st `  (
h `  ( i  +  1 ) ) ) )
106100, 105wceq 1623 . . . . . . . . . . . . . . 15  wff  ( f `
 ( 2nd `  (
h `  i )
) )  =  ( f `  ( 1st `  ( h `  (
i  +  1 ) ) ) )
107 cmin 9037 . . . . . . . . . . . . . . . . 17  class  -
10889, 80, 107co 5858 . . . . . . . . . . . . . . . 16  class  ( n  -  1 )
109 cfz 10782 . . . . . . . . . . . . . . . 16  class  ...
11080, 108, 109co 5858 . . . . . . . . . . . . . . 15  class  ( 1 ... ( n  - 
1 ) )
111106, 96, 110wral 2543 . . . . . . . . . . . . . 14  wff  A. i  e.  ( 1 ... (
n  -  1 ) ) ( f `  ( 2nd `  ( h `
 i ) ) )  =  ( f `
 ( 1st `  (
h `  ( i  +  1 ) ) ) )
11288, 95, 111w3a 934 . . . . . . . . . . . . 13  wff  ( ( f `  ( 1st `  ( h `  1
) ) )  =  x  /\  ( f `
 ( 2nd `  (
h `  n )
) )  =  y  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( f `  ( 2nd `  ( h `
 i ) ) )  =  ( f `
 ( 1st `  (
h `  ( i  +  1 ) ) ) ) )
11317, 17cxp 4687 . . . . . . . . . . . . . 14  class  ( v  X.  v )
11480, 89, 109co 5858 . . . . . . . . . . . . . 14  class  ( 1 ... n )
115 cmap 6772 . . . . . . . . . . . . . 14  class  ^m
116113, 114, 115co 5858 . . . . . . . . . . . . 13  class  ( ( v  X.  v )  ^m  ( 1 ... n ) )
117112, 81, 116crab 2547 . . . . . . . . . . . 12  class  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }
118 cxrs 13399 . . . . . . . . . . . . 13  class  RR* s
1196, 74cfv 5255 . . . . . . . . . . . . . 14  class  ( dist `  r )
12079cv 1622 . . . . . . . . . . . . . 14  class  g
121119, 120ccom 4693 . . . . . . . . . . . . 13  class  ( (
dist `  r )  o.  g )
122 cgsu 13401 . . . . . . . . . . . . 13  class  gsumg
123118, 121, 122co 5858 . . . . . . . . . . . 12  class  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) )
12479, 117, 123cmpt 4077 . . . . . . . . . . 11  class  ( g  e.  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) )
125124crn 4690 . . . . . . . . . 10  class  ran  (
g  e.  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) )
12677, 78, 125ciun 3905 . . . . . . . . 9  class  U_ n  e.  NN  ran  ( g  e.  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) )
127 cxr 8866 . . . . . . . . 9  class  RR*
128 clt 8867 . . . . . . . . . 10  class  <
129128ccnv 4688 . . . . . . . . 9  class  `'  <
130126, 127, 129csup 7193 . . . . . . . 8  class  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  )
13149, 76, 12, 12, 130cmpt2 5860 . . . . . . 7  class  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) )
13275, 131cop 3643 . . . . . 6  class  <. ( dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >.
13366, 73, 132ctp 3642 . . . . 5  class  { <. (TopSet `  ndx ) ,  ( ( TopOpen `  r ) qTop  f ) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r ) )  o.  `' f ) >. ,  <. ( dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  { h  e.  ( ( v  X.  v )  ^m  (
1 ... n ) )  |  ( ( f `
 ( 1st `  (
h `  1 )
) )  =  x  /\  ( f `  ( 2nd `  ( h `
 n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. }
13459, 133cun 3150 . . . 4  class  ( ( { <. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. } >. ,  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } )
1355, 8, 134csb 3081 . . 3  class  [_ ( Base `  r )  / 
v ]_ ( ( {
<. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. } >. ,  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } )
1362, 3, 4, 4, 135cmpt2 5860 . 2  class  ( f  e.  _V ,  r  e.  _V  |->  [_ ( Base `  r )  / 
v ]_ ( ( {
<. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. } >. ,  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } ) )
1371, 136wceq 1623 1  wff  "s  =  (
f  e.  _V , 
r  e.  _V  |->  [_ ( Base `  r )  /  v ]_ (
( { <. ( Base `  ndx ) ,  ran  f >. ,  <. ( +g  `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >. ,  <. ( .r `  ndx ) ,  U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >. }  u.  { <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >. ,  <. ( .s `  ndx ) ,  U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >. } )  u. 
{ <. (TopSet `  ndx ) ,  ( ( TopOpen
`  r ) qTop  f
) >. ,  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >. ,  <. (
dist `  ndx ) ,  ( x  e.  ran  f ,  y  e.  ran  f  |->  sup ( U_ n  e.  NN  ran  ( g  e.  {
h  e.  ( ( v  X.  v )  ^m  ( 1 ... n ) )  |  ( ( f `  ( 1st `  ( h `
 1 ) ) )  =  x  /\  ( f `  ( 2nd `  ( h `  n ) ) )  =  y  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( f `  ( 2nd `  ( h `  i
) ) )  =  ( f `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  |->  ( RR* s  gsumg  ( ( dist `  r
)  o.  g ) ) ) ,  RR* ,  `'  <  ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  imasval  13414
  Copyright terms: Public domain W3C validator