Definition df-imas 13689

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 4850, 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 4849) and/or R ( with df-ress 13431) 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

Step	Hyp	Ref	Expression
1		cimas 13685	. 2 class "s
2		vf	. . 3 set f
3		vr	. . 3 set r
4		cvv 2916	. . 3 class _V
5		vv	. . . 4 set v
6	3	cv 1648	. . . . 5 class r
7		cbs 13424	. . . . 5 class Base
8	6, 7	cfv 5413	. . . 4 class ( Base ` r )
9		cnx 13421	. . . . . . . . 9 class ndx
10	9, 7	cfv 5413	. . . . . . . 8 class ( Base ` ndx )
11	2	cv 1648	. . . . . . . . 9 class f
12	11	crn 4838	. . . . . . . 8 class ran f
13	10, 12	cop 3777	. . . . . . 7 class <. ( Base ` ndx ) , ran f >.
14		cplusg 13484	. . . . . . . . 9 class +g
15	9, 14	cfv 5413	. . . . . . . 8 class ( +g ` ndx )
16		vp	. . . . . . . . 9 set p
17	5	cv 1648	. . . . . . . . 9 class v
18		vq	. . . . . . . . . 10 set q
19	16	cv 1648	. . . . . . . . . . . . . 14 class p
20	19, 11	cfv 5413	. . . . . . . . . . . . 13 class ( f ` p )
21	18	cv 1648	. . . . . . . . . . . . . 14 class q
22	21, 11	cfv 5413	. . . . . . . . . . . . 13 class ( f ` q )
23	20, 22	cop 3777	. . . . . . . . . . . 12 class <. ( f ` p ) , ( f ` q ) >.
24	6, 14	cfv 5413	. . . . . . . . . . . . . 14 class ( +g ` r )
25	19, 21, 24	co 6040	. . . . . . . . . . . . 13 class ( p ( +g ` r ) q )
26	25, 11	cfv 5413	. . . . . . . . . . . 12 class ( f ` ( p ( +g ` r ) q ) )
27	23, 26	cop 3777	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >.
28	27	csn 3774	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
29	18, 17, 28	ciun 4053	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
30	16, 17, 29	ciun 4053	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
31	15, 30	cop 3777	. . . . . . 7 class <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >.
32		cmulr 13485	. . . . . . . . 9 class .r
33	9, 32	cfv 5413	. . . . . . . 8 class ( .r ` ndx )
34	6, 32	cfv 5413	. . . . . . . . . . . . . 14 class ( .r ` r )
35	19, 21, 34	co 6040	. . . . . . . . . . . . 13 class ( p ( .r ` r ) q )
36	35, 11	cfv 5413	. . . . . . . . . . . 12 class ( f ` ( p ( .r ` r ) q ) )
37	23, 36	cop 3777	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >.
38	37	csn 3774	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
39	18, 17, 38	ciun 4053	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
40	16, 17, 39	ciun 4053	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
41	33, 40	cop 3777	. . . . . . 7 class <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >.
42	13, 31, 41	ctp 3776	. . . . . 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 13487	. . . . . . . . 9 class Scalar
44	9, 43	cfv 5413	. . . . . . . 8 class (Scalar ` ndx )
45	6, 43	cfv 5413	. . . . . . . 8 class (Scalar ` r )
46	44, 45	cop 3777	. . . . . . 7 class <. (Scalar ` ndx ) , (Scalar ` r ) >.
47		cvsca 13488	. . . . . . . . 9 class .s
48	9, 47	cfv 5413	. . . . . . . 8 class ( .s ` ndx )
49		vx	. . . . . . . . . 10 set x
50	45, 7	cfv 5413	. . . . . . . . . 10 class ( Base ` (Scalar ` r ) )
51	22	csn 3774	. . . . . . . . . 10 class { ( f ` q ) }
52	6, 47	cfv 5413	. . . . . . . . . . . 12 class ( .s ` r )
53	19, 21, 52	co 6040	. . . . . . . . . . 11 class ( p ( .s ` r ) q )
54	53, 11	cfv 5413	. . . . . . . . . 10 class ( f ` ( p ( .s ` r ) q ) )
55	16, 49, 50, 51, 54	cmpt2 6042	. . . . . . . . 9 class ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
56	18, 17, 55	ciun 4053	. . . . . . . 8 class U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
57	48, 56	cop 3777	. . . . . . 7 class <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >.
58	46, 57	cpr 3775	. . . . . 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 ) ) ) >. }
59	42, 58	cun 3278	. . . . 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 13490	. . . . . . . 8 class TopSet
61	9, 60	cfv 5413	. . . . . . 7 class (TopSet ` ndx )
62		ctopn 13604	. . . . . . . . 9 class TopOpen
63	6, 62	cfv 5413	. . . . . . . 8 class ( TopOpen ` r )
64		cqtop 13684	. . . . . . . 8 class qTop
65	63, 11, 64	co 6040	. . . . . . 7 class ( ( TopOpen ` r ) qTop f )
66	61, 65	cop 3777	. . . . . 6 class <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >.
67		cple 13491	. . . . . . . 8 class le
68	9, 67	cfv 5413	. . . . . . 7 class ( le ` ndx )
69	6, 67	cfv 5413	. . . . . . . . 9 class ( le ` r )
70	11, 69	ccom 4841	. . . . . . . 8 class ( f o. ( le ` r ) )
71	11	ccnv 4836	. . . . . . . 8 class `' f
72	70, 71	ccom 4841	. . . . . . 7 class ( ( f o. ( le ` r ) ) o. `' f )
73	68, 72	cop 3777	. . . . . 6 class <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >.
74		cds 13493	. . . . . . . 8 class dist
75	9, 74	cfv 5413	. . . . . . 7 class ( dist ` ndx )
76		vy	. . . . . . . 8 set y
77		vn	. . . . . . . . . 10 set n
78		cn 9956	. . . . . . . . . 10 class NN
79		vg	. . . . . . . . . . . 12 set g
80		c1 8947	. . . . . . . . . . . . . . . . . 18 class 1
81		vh	. . . . . . . . . . . . . . . . . . 19 set h
82	81	cv 1648	. . . . . . . . . . . . . . . . . 18 class h
83	80, 82	cfv 5413	. . . . . . . . . . . . . . . . 17 class ( h ` 1 )
84		c1st 6306	. . . . . . . . . . . . . . . . 17 class 1st
85	83, 84	cfv 5413	. . . . . . . . . . . . . . . 16 class ( 1st ` ( h ` 1 ) )
86	85, 11	cfv 5413	. . . . . . . . . . . . . . 15 class ( f ` ( 1st ` ( h ` 1 ) ) )
87	49	cv 1648	. . . . . . . . . . . . . . 15 class x
88	86, 87	wceq 1649	. . . . . . . . . . . . . 14 wff ( f ` ( 1st ` ( h ` 1 ) ) ) = x
89	77	cv 1648	. . . . . . . . . . . . . . . . . 18 class n
90	89, 82	cfv 5413	. . . . . . . . . . . . . . . . 17 class ( h ` n )
91		c2nd 6307	. . . . . . . . . . . . . . . . 17 class 2nd
92	90, 91	cfv 5413	. . . . . . . . . . . . . . . 16 class ( 2nd ` ( h ` n ) )
93	92, 11	cfv 5413	. . . . . . . . . . . . . . 15 class ( f ` ( 2nd ` ( h ` n ) ) )
94	76	cv 1648	. . . . . . . . . . . . . . 15 class y
95	93, 94	wceq 1649	. . . . . . . . . . . . . 14 wff ( f ` ( 2nd ` ( h ` n ) ) ) = y
96		vi	. . . . . . . . . . . . . . . . . . . 20 set i
97	96	cv 1648	. . . . . . . . . . . . . . . . . . 19 class i
98	97, 82	cfv 5413	. . . . . . . . . . . . . . . . . 18 class ( h ` i )
99	98, 91	cfv 5413	. . . . . . . . . . . . . . . . 17 class ( 2nd ` ( h ` i ) )
100	99, 11	cfv 5413	. . . . . . . . . . . . . . . 16 class ( f ` ( 2nd ` ( h ` i ) ) )
101		caddc 8949	. . . . . . . . . . . . . . . . . . . 20 class +
102	97, 80, 101	co 6040	. . . . . . . . . . . . . . . . . . 19 class ( i + 1 )
103	102, 82	cfv 5413	. . . . . . . . . . . . . . . . . 18 class ( h ` ( i + 1 ) )
104	103, 84	cfv 5413	. . . . . . . . . . . . . . . . 17 class ( 1st ` ( h ` ( i + 1 ) ) )
105	104, 11	cfv 5413	. . . . . . . . . . . . . . . 16 class ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
106	100, 105	wceq 1649	. . . . . . . . . . . . . . 15 wff ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
107		cmin 9247	. . . . . . . . . . . . . . . . 17 class -
108	89, 80, 107	co 6040	. . . . . . . . . . . . . . . 16 class ( n - 1 )
109		cfz 10999	. . . . . . . . . . . . . . . 16 class ...
110	80, 108, 109	co 6040	. . . . . . . . . . . . . . 15 class ( 1 ... ( n - 1 ) )
111	106, 96, 110	wral 2666	. . . . . . . . . . . . . 14 wff A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
112	88, 95, 111	w3a 936	. . . . . . . . . . . . 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 ) ) ) ) )
113	17, 17	cxp 4835	. . . . . . . . . . . . . 14 class ( v X. v )
114	80, 89, 109	co 6040	. . . . . . . . . . . . . 14 class ( 1 ... n )
115		cmap 6977	. . . . . . . . . . . . . 14 class ^m
116	113, 114, 115	co 6040	. . . . . . . . . . . . 13 class ( ( v X. v ) ^m ( 1 ... n ) )
117	112, 81, 116	crab 2670	. . . . . . . . . . . 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 13677	. . . . . . . . . . . . 13 class RR* s
119	6, 74	cfv 5413	. . . . . . . . . . . . . 14 class ( dist ` r )
120	79	cv 1648	. . . . . . . . . . . . . 14 class g
121	119, 120	ccom 4841	. . . . . . . . . . . . 13 class ( ( dist ` r ) o. g )
122		cgsu 13679	. . . . . . . . . . . . 13 class gsumg
123	118, 121, 122	co 6040	. . . . . . . . . . . 12 class ( RR* s gsumg ( ( dist ` r ) o. g ) )
124	79, 117, 123	cmpt 4226	. . . . . . . . . . 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 ) ) )
125	124	crn 4838	. . . . . . . . . 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 ) ) )
126	77, 78, 125	ciun 4053	. . . . . . . . 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 9075	. . . . . . . . 9 class RR*
128		clt 9076	. . . . . . . . . 10 class <
129	128	ccnv 4836	. . . . . . . . 9 class `' <
130	126, 127, 129	csup 7403	. . . . . . . 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* , `' < )
131	49, 76, 12, 12, 130	cmpt2 6042	. . . . . . 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* , `' < ) )
132	75, 131	cop 3777	. . . . . 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* , `' < ) ) >.
133	66, 73, 132	ctp 3776	. . . . 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* , `' < ) ) >. }
134	59, 133	cun 3278	. . . 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* , `' < ) ) >. } )
135	5, 8, 134	csb 3211	. . 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* , `' < ) ) >. } )
136	2, 3, 4, 4, 135	cmpt2 6042	. 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* , `' < ) ) >. } ) )
137	1, 136	wceq 1649	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* , `' < ) ) >. } ) )

This definition is referenced by:  imasval  13692