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

Definition df-imas 14568
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 4964, 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 4963) and/or  R ( with df-ress 14302) 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  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 14564 . 2  class  "s
2 vf . . 3  setvar  f
3 vr . . 3  setvar  r
4 cvv 3078 . . 3  class  _V
5 vv . . . 4  setvar  v
63cv 1369 . . . . 5  class  r
7 cbs 14295 . . . . 5  class  Base
86, 7cfv 5529 . . . 4  class  ( Base `  r )
9 cnx 14292 . . . . . . . . 9  class  ndx
109, 7cfv 5529 . . . . . . . 8  class  ( Base `  ndx )
112cv 1369 . . . . . . . . 9  class  f
1211crn 4952 . . . . . . . 8  class  ran  f
1310, 12cop 3994 . . . . . . 7  class  <. ( Base `  ndx ) ,  ran  f >.
14 cplusg 14360 . . . . . . . . 9  class  +g
159, 14cfv 5529 . . . . . . . 8  class  ( +g  ` 
ndx )
16 vp . . . . . . . . 9  setvar  p
175cv 1369 . . . . . . . . 9  class  v
18 vq . . . . . . . . . 10  setvar  q
1916cv 1369 . . . . . . . . . . . . . 14  class  p
2019, 11cfv 5529 . . . . . . . . . . . . 13  class  ( f `
 p )
2118cv 1369 . . . . . . . . . . . . . 14  class  q
2221, 11cfv 5529 . . . . . . . . . . . . 13  class  ( f `
 q )
2320, 22cop 3994 . . . . . . . . . . . 12  class  <. (
f `  p ) ,  ( f `  q ) >.
246, 14cfv 5529 . . . . . . . . . . . . . 14  class  ( +g  `  r )
2519, 21, 24co 6203 . . . . . . . . . . . . 13  class  ( p ( +g  `  r
) q )
2625, 11cfv 5529 . . . . . . . . . . . 12  class  ( f `
 ( p ( +g  `  r ) q ) )
2723, 26cop 3994 . . . . . . . . . . 11  class  <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>.
2827csn 3988 . . . . . . . . . 10  class  { <. <.
( f `  p
) ,  ( f `
 q ) >. ,  ( f `  ( p ( +g  `  r ) q ) ) >. }
2918, 17, 28ciun 4282 . . . . . . . . 9  class  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. }
3016, 17, 29ciun 4282 . . . . . . . 8  class  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( +g  `  r
) q ) )
>. }
3115, 30cop 3994 . . . . . . 7  class  <. ( +g  `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( +g  `  r ) q ) ) >. } >.
32 cmulr 14361 . . . . . . . . 9  class  .r
339, 32cfv 5529 . . . . . . . 8  class  ( .r
`  ndx )
346, 32cfv 5529 . . . . . . . . . . . . . 14  class  ( .r
`  r )
3519, 21, 34co 6203 . . . . . . . . . . . . 13  class  ( p ( .r `  r
) q )
3635, 11cfv 5529 . . . . . . . . . . . 12  class  ( f `
 ( p ( .r `  r ) q ) )
3723, 36cop 3994 . . . . . . . . . . 11  class  <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>.
3837csn 3988 . . . . . . . . . 10  class  { <. <.
( f `  p
) ,  ( f `
 q ) >. ,  ( f `  ( p ( .r
`  r ) q ) ) >. }
3918, 17, 38ciun 4282 . . . . . . . . 9  class  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>. }
4016, 17, 39ciun 4282 . . . . . . . 8  class  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( f `  ( p ( .r `  r
) q ) )
>. }
4133, 40cop 3994 . . . . . . 7  class  <. ( .r `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( f `  ( p ( .r
`  r ) q ) ) >. } >.
4213, 31, 41ctp 3992 . . . . . 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 14363 . . . . . . . . 9  class Scalar
449, 43cfv 5529 . . . . . . . 8  class  (Scalar `  ndx )
456, 43cfv 5529 . . . . . . . 8  class  (Scalar `  r )
4644, 45cop 3994 . . . . . . 7  class  <. (Scalar ` 
ndx ) ,  (Scalar `  r ) >.
47 cvsca 14364 . . . . . . . . 9  class  .s
489, 47cfv 5529 . . . . . . . 8  class  ( .s
`  ndx )
49 vx . . . . . . . . . 10  setvar  x
5045, 7cfv 5529 . . . . . . . . . 10  class  ( Base `  (Scalar `  r )
)
5122csn 3988 . . . . . . . . . 10  class  { ( f `  q ) }
526, 47cfv 5529 . . . . . . . . . . . 12  class  ( .s
`  r )
5319, 21, 52co 6203 . . . . . . . . . . 11  class  ( p ( .s `  r
) q )
5453, 11cfv 5529 . . . . . . . . . 10  class  ( f `
 ( p ( .s `  r ) q ) )
5516, 49, 50, 51, 54cmpt2 6205 . . . . . . . . 9  class  ( p  e.  ( Base `  (Scalar `  r ) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s
`  r ) q ) ) )
5618, 17, 55ciun 4282 . . . . . . . 8  class  U_ q  e.  v  ( p  e.  ( Base `  (Scalar `  r ) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s
`  r ) q ) ) )
5748, 56cop 3994 . . . . . . 7  class  <. ( .s `  ndx ) , 
U_ q  e.  v  ( p  e.  (
Base `  (Scalar `  r
) ) ,  x  e.  { ( f `  q ) }  |->  ( f `  ( p ( .s `  r
) q ) ) ) >.
58 cip 14365 . . . . . . . . 9  class  .i
599, 58cfv 5529 . . . . . . . 8  class  ( .i
`  ndx )
606, 58cfv 5529 . . . . . . . . . . . . 13  class  ( .i
`  r )
6119, 21, 60co 6203 . . . . . . . . . . . 12  class  ( p ( .i `  r
) q )
6223, 61cop 3994 . . . . . . . . . . 11  class  <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( p ( .i `  r ) q )
>.
6362csn 3988 . . . . . . . . . 10  class  { <. <.
( f `  p
) ,  ( f `
 q ) >. ,  ( p ( .i `  r ) q ) >. }
6418, 17, 63ciun 4282 . . . . . . . . 9  class  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( p ( .i `  r ) q )
>. }
6516, 17, 64ciun 4282 . . . . . . . 8  class  U_ p  e.  v  U_ q  e.  v  { <. <. (
f `  p ) ,  ( f `  q ) >. ,  ( p ( .i `  r ) q )
>. }
6659, 65cop 3994 . . . . . . 7  class  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  r
) q ) >. } >.
6746, 57, 66ctp 3992 . . . . . 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  r
) q ) >. } >. }
6842, 67cun 3437 . . . . 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  r
) q ) >. } >. } )
69 cts 14366 . . . . . . . 8  class TopSet
709, 69cfv 5529 . . . . . . 7  class  (TopSet `  ndx )
71 ctopn 14482 . . . . . . . . 9  class  TopOpen
726, 71cfv 5529 . . . . . . . 8  class  ( TopOpen `  r )
73 cqtop 14563 . . . . . . . 8  class qTop
7472, 11, 73co 6203 . . . . . . 7  class  ( (
TopOpen `  r ) qTop  f
)
7570, 74cop 3994 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  ( ( TopOpen `  r ) qTop  f ) >.
76 cple 14367 . . . . . . . 8  class  le
779, 76cfv 5529 . . . . . . 7  class  ( le
`  ndx )
786, 76cfv 5529 . . . . . . . . 9  class  ( le
`  r )
7911, 78ccom 4955 . . . . . . . 8  class  ( f  o.  ( le `  r ) )
8011ccnv 4950 . . . . . . . 8  class  `' f
8179, 80ccom 4955 . . . . . . 7  class  ( ( f  o.  ( le
`  r ) )  o.  `' f )
8277, 81cop 3994 . . . . . 6  class  <. ( le `  ndx ) ,  ( ( f  o.  ( le `  r
) )  o.  `' f ) >.
83 cds 14369 . . . . . . . 8  class  dist
849, 83cfv 5529 . . . . . . 7  class  ( dist `  ndx )
85 vy . . . . . . . 8  setvar  y
86 vn . . . . . . . . . 10  setvar  n
87 cn 10436 . . . . . . . . . 10  class  NN
88 vg . . . . . . . . . . . 12  setvar  g
89 c1 9397 . . . . . . . . . . . . . . . . . 18  class  1
90 vh . . . . . . . . . . . . . . . . . . 19  setvar  h
9190cv 1369 . . . . . . . . . . . . . . . . . 18  class  h
9289, 91cfv 5529 . . . . . . . . . . . . . . . . 17  class  ( h `
 1 )
93 c1st 6688 . . . . . . . . . . . . . . . . 17  class  1st
9492, 93cfv 5529 . . . . . . . . . . . . . . . 16  class  ( 1st `  ( h `  1
) )
9594, 11cfv 5529 . . . . . . . . . . . . . . 15  class  ( f `
 ( 1st `  (
h `  1 )
) )
9649cv 1369 . . . . . . . . . . . . . . 15  class  x
9795, 96wceq 1370 . . . . . . . . . . . . . 14  wff  ( f `
 ( 1st `  (
h `  1 )
) )  =  x
9886cv 1369 . . . . . . . . . . . . . . . . . 18  class  n
9998, 91cfv 5529 . . . . . . . . . . . . . . . . 17  class  ( h `
 n )
100 c2nd 6689 . . . . . . . . . . . . . . . . 17  class  2nd
10199, 100cfv 5529 . . . . . . . . . . . . . . . 16  class  ( 2nd `  ( h `  n
) )
102101, 11cfv 5529 . . . . . . . . . . . . . . 15  class  ( f `
 ( 2nd `  (
h `  n )
) )
10385cv 1369 . . . . . . . . . . . . . . 15  class  y
104102, 103wceq 1370 . . . . . . . . . . . . . 14  wff  ( f `
 ( 2nd `  (
h `  n )
) )  =  y
105 vi . . . . . . . . . . . . . . . . . . . 20  setvar  i
106105cv 1369 . . . . . . . . . . . . . . . . . . 19  class  i
107106, 91cfv 5529 . . . . . . . . . . . . . . . . . 18  class  ( h `
 i )
108107, 100cfv 5529 . . . . . . . . . . . . . . . . 17  class  ( 2nd `  ( h `  i
) )
109108, 11cfv 5529 . . . . . . . . . . . . . . . 16  class  ( f `
 ( 2nd `  (
h `  i )
) )
110 caddc 9399 . . . . . . . . . . . . . . . . . . . 20  class  +
111106, 89, 110co 6203 . . . . . . . . . . . . . . . . . . 19  class  ( i  +  1 )
112111, 91cfv 5529 . . . . . . . . . . . . . . . . . 18  class  ( h `
 ( i  +  1 ) )
113112, 93cfv 5529 . . . . . . . . . . . . . . . . 17  class  ( 1st `  ( h `  (
i  +  1 ) ) )
114113, 11cfv 5529 . . . . . . . . . . . . . . . 16  class  ( f `
 ( 1st `  (
h `  ( i  +  1 ) ) ) )
115109, 114wceq 1370 . . . . . . . . . . . . . . 15  wff  ( f `
 ( 2nd `  (
h `  i )
) )  =  ( f `  ( 1st `  ( h `  (
i  +  1 ) ) ) )
116 cmin 9709 . . . . . . . . . . . . . . . . 17  class  -
11798, 89, 116co 6203 . . . . . . . . . . . . . . . 16  class  ( n  -  1 )
118 cfz 11557 . . . . . . . . . . . . . . . 16  class  ...
11989, 117, 118co 6203 . . . . . . . . . . . . . . 15  class  ( 1 ... ( n  - 
1 ) )
120115, 105, 119wral 2799 . . . . . . . . . . . . . 14  wff  A. i  e.  ( 1 ... (
n  -  1 ) ) ( f `  ( 2nd `  ( h `
 i ) ) )  =  ( f `
 ( 1st `  (
h `  ( i  +  1 ) ) ) )
12197, 104, 120w3a 965 . . . . . . . . . . . . 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 ) ) ) ) )
12217, 17cxp 4949 . . . . . . . . . . . . . 14  class  ( v  X.  v )
12389, 98, 118co 6203 . . . . . . . . . . . . . 14  class  ( 1 ... n )
124 cmap 7327 . . . . . . . . . . . . . 14  class  ^m
125122, 123, 124co 6203 . . . . . . . . . . . . 13  class  ( ( v  X.  v )  ^m  ( 1 ... n ) )
126121, 90, 125crab 2803 . . . . . . . . . . . 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 ) ) ) ) ) }
127 cxrs 14560 . . . . . . . . . . . . 13  class  RR*s
1286, 83cfv 5529 . . . . . . . . . . . . . 14  class  ( dist `  r )
12988cv 1369 . . . . . . . . . . . . . 14  class  g
130128, 129ccom 4955 . . . . . . . . . . . . 13  class  ( (
dist `  r )  o.  g )
131 cgsu 14501 . . . . . . . . . . . . 13  class  gsumg
132127, 130, 131co 6203 . . . . . . . . . . . 12  class  ( RR*s  gsumg  ( ( dist `  r
)  o.  g ) )
13388, 126, 132cmpt 4461 . . . . . . . . . . 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 ) ) )
134133crn 4952 . . . . . . . . . 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 ) ) )
13586, 87, 134ciun 4282 . . . . . . . . 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 ) ) )
136 cxr 9531 . . . . . . . . 9  class  RR*
137 clt 9532 . . . . . . . . . 10  class  <
138137ccnv 4950 . . . . . . . . 9  class  `'  <
139135, 136, 138csup 7804 . . . . . . . 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* ,  `'  <  )
14049, 85, 12, 12, 139cmpt2 6205 . . . . . . 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* ,  `'  <  ) )
14184, 140cop 3994 . . . . . 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* ,  `'  <  ) ) >.
14275, 82, 141ctp 3992 . . . . 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* ,  `'  <  ) ) >. }
14368, 142cun 3437 . . . 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  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* ,  `'  <  ) ) >. } )
1445, 8, 143csb 3398 . . 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  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* ,  `'  <  ) ) >. } )
1452, 3, 4, 4, 144cmpt2 6205 . 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  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* ,  `'  <  ) ) >. } ) )
1461, 145wceq 1370 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 ) ) ) >. ,  <. ( .i `  ndx ) , 
U_ p  e.  v 
U_ q  e.  v  { <. <. ( f `  p ) ,  ( f `  q )
>. ,  ( p
( .i `  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 setvar class
This definition is referenced by:  imasval  14571
  Copyright terms: Public domain W3C validator