Definition df-imas 14886

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 5002, 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 5001) and/or R ( with df-ress 14620) 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

Step	Hyp	Ref	Expression
1		cimas 14882	. 2 class "s
2		vf	. . 3 setvar f
3		vr	. . 3 setvar r
4		cvv 3095	. . 3 class _V
5		vv	. . . 4 setvar v
6	3	cv 1382	. . . . 5 class r
7		cbs 14613	. . . . 5 class Base
8	6, 7	cfv 5578	. . . 4 class ( Base ` r )
9		cnx 14610	. . . . . . . . 9 class ndx
10	9, 7	cfv 5578	. . . . . . . 8 class ( Base ` ndx )
11	2	cv 1382	. . . . . . . . 9 class f
12	11	crn 4990	. . . . . . . 8 class ran f
13	10, 12	cop 4020	. . . . . . 7 class <. ( Base ` ndx ) , ran f >.
14		cplusg 14678	. . . . . . . . 9 class +g
15	9, 14	cfv 5578	. . . . . . . 8 class ( +g ` ndx )
16		vp	. . . . . . . . 9 setvar p
17	5	cv 1382	. . . . . . . . 9 class v
18		vq	. . . . . . . . . 10 setvar q
19	16	cv 1382	. . . . . . . . . . . . . 14 class p
20	19, 11	cfv 5578	. . . . . . . . . . . . 13 class ( f ` p )
21	18	cv 1382	. . . . . . . . . . . . . 14 class q
22	21, 11	cfv 5578	. . . . . . . . . . . . 13 class ( f ` q )
23	20, 22	cop 4020	. . . . . . . . . . . 12 class <. ( f ` p ) , ( f ` q ) >.
24	6, 14	cfv 5578	. . . . . . . . . . . . . 14 class ( +g ` r )
25	19, 21, 24	co 6281	. . . . . . . . . . . . 13 class ( p ( +g ` r ) q )
26	25, 11	cfv 5578	. . . . . . . . . . . 12 class ( f ` ( p ( +g ` r ) q ) )
27	23, 26	cop 4020	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >.
28	27	csn 4014	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
29	18, 17, 28	ciun 4315	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
30	16, 17, 29	ciun 4315	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
31	15, 30	cop 4020	. . . . . . 7 class <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >.
32		cmulr 14679	. . . . . . . . 9 class .r
33	9, 32	cfv 5578	. . . . . . . 8 class ( .r ` ndx )
34	6, 32	cfv 5578	. . . . . . . . . . . . . 14 class ( .r ` r )
35	19, 21, 34	co 6281	. . . . . . . . . . . . 13 class ( p ( .r ` r ) q )
36	35, 11	cfv 5578	. . . . . . . . . . . 12 class ( f ` ( p ( .r ` r ) q ) )
37	23, 36	cop 4020	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >.
38	37	csn 4014	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
39	18, 17, 38	ciun 4315	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
40	16, 17, 39	ciun 4315	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
41	33, 40	cop 4020	. . . . . . 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 4018	. . . . . 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 14681	. . . . . . . . 9 class Scalar
44	9, 43	cfv 5578	. . . . . . . 8 class (Scalar ` ndx )
45	6, 43	cfv 5578	. . . . . . . 8 class (Scalar ` r )
46	44, 45	cop 4020	. . . . . . 7 class <. (Scalar ` ndx ) , (Scalar ` r ) >.
47		cvsca 14682	. . . . . . . . 9 class .s
48	9, 47	cfv 5578	. . . . . . . 8 class ( .s ` ndx )
49		vx	. . . . . . . . . 10 setvar x
50	45, 7	cfv 5578	. . . . . . . . . 10 class ( Base ` (Scalar ` r ) )
51	22	csn 4014	. . . . . . . . . 10 class { ( f ` q ) }
52	6, 47	cfv 5578	. . . . . . . . . . . 12 class ( .s ` r )
53	19, 21, 52	co 6281	. . . . . . . . . . 11 class ( p ( .s ` r ) q )
54	53, 11	cfv 5578	. . . . . . . . . 10 class ( f ` ( p ( .s ` r ) q ) )
55	16, 49, 50, 51, 54	cmpt2 6283	. . . . . . . . 9 class ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
56	18, 17, 55	ciun 4315	. . . . . . . 8 class U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
57	48, 56	cop 4020	. . . . . . 7 class <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >.
58		cip 14683	. . . . . . . . 9 class .i
59	9, 58	cfv 5578	. . . . . . . 8 class ( .i ` ndx )
60	6, 58	cfv 5578	. . . . . . . . . . . . 13 class ( .i ` r )
61	19, 21, 60	co 6281	. . . . . . . . . . . 12 class ( p ( .i ` r ) q )
62	23, 61	cop 4020	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >.
63	62	csn 4014	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
64	18, 17, 63	ciun 4315	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
65	16, 17, 64	ciun 4315	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
66	59, 65	cop 4020	. . . . . . 7 class <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >.
67	46, 57, 66	ctp 4018	. . . . . 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 ) >. } >. }
68	42, 67	cun 3459	. . . . 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 14684	. . . . . . . 8 class TopSet
70	9, 69	cfv 5578	. . . . . . 7 class (TopSet ` ndx )
71		ctopn 14800	. . . . . . . . 9 class TopOpen
72	6, 71	cfv 5578	. . . . . . . 8 class ( TopOpen ` r )
73		cqtop 14881	. . . . . . . 8 class qTop
74	72, 11, 73	co 6281	. . . . . . 7 class ( ( TopOpen ` r ) qTop f )
75	70, 74	cop 4020	. . . . . 6 class <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >.
76		cple 14685	. . . . . . . 8 class le
77	9, 76	cfv 5578	. . . . . . 7 class ( le ` ndx )
78	6, 76	cfv 5578	. . . . . . . . 9 class ( le ` r )
79	11, 78	ccom 4993	. . . . . . . 8 class ( f o. ( le ` r ) )
80	11	ccnv 4988	. . . . . . . 8 class `' f
81	79, 80	ccom 4993	. . . . . . 7 class ( ( f o. ( le ` r ) ) o. `' f )
82	77, 81	cop 4020	. . . . . 6 class <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >.
83		cds 14687	. . . . . . . 8 class dist
84	9, 83	cfv 5578	. . . . . . 7 class ( dist ` ndx )
85		vy	. . . . . . . 8 setvar y
86		vn	. . . . . . . . . 10 setvar n
87		cn 10543	. . . . . . . . . 10 class NN
88		vg	. . . . . . . . . . . 12 setvar g
89		c1 9496	. . . . . . . . . . . . . . . . . 18 class 1
90		vh	. . . . . . . . . . . . . . . . . . 19 setvar h
91	90	cv 1382	. . . . . . . . . . . . . . . . . 18 class h
92	89, 91	cfv 5578	. . . . . . . . . . . . . . . . 17 class ( h ` 1 )
93		c1st 6783	. . . . . . . . . . . . . . . . 17 class 1st
94	92, 93	cfv 5578	. . . . . . . . . . . . . . . 16 class ( 1st ` ( h ` 1 ) )
95	94, 11	cfv 5578	. . . . . . . . . . . . . . 15 class ( f ` ( 1st ` ( h ` 1 ) ) )
96	49	cv 1382	. . . . . . . . . . . . . . 15 class x
97	95, 96	wceq 1383	. . . . . . . . . . . . . 14 wff ( f ` ( 1st ` ( h ` 1 ) ) ) = x
98	86	cv 1382	. . . . . . . . . . . . . . . . . 18 class n
99	98, 91	cfv 5578	. . . . . . . . . . . . . . . . 17 class ( h ` n )
100		c2nd 6784	. . . . . . . . . . . . . . . . 17 class 2nd
101	99, 100	cfv 5578	. . . . . . . . . . . . . . . 16 class ( 2nd ` ( h ` n ) )
102	101, 11	cfv 5578	. . . . . . . . . . . . . . 15 class ( f ` ( 2nd ` ( h ` n ) ) )
103	85	cv 1382	. . . . . . . . . . . . . . 15 class y
104	102, 103	wceq 1383	. . . . . . . . . . . . . 14 wff ( f ` ( 2nd ` ( h ` n ) ) ) = y
105		vi	. . . . . . . . . . . . . . . . . . . 20 setvar i
106	105	cv 1382	. . . . . . . . . . . . . . . . . . 19 class i
107	106, 91	cfv 5578	. . . . . . . . . . . . . . . . . 18 class ( h ` i )
108	107, 100	cfv 5578	. . . . . . . . . . . . . . . . 17 class ( 2nd ` ( h ` i ) )
109	108, 11	cfv 5578	. . . . . . . . . . . . . . . 16 class ( f ` ( 2nd ` ( h ` i ) ) )
110		caddc 9498	. . . . . . . . . . . . . . . . . . . 20 class +
111	106, 89, 110	co 6281	. . . . . . . . . . . . . . . . . . 19 class ( i + 1 )
112	111, 91	cfv 5578	. . . . . . . . . . . . . . . . . 18 class ( h ` ( i + 1 ) )
113	112, 93	cfv 5578	. . . . . . . . . . . . . . . . 17 class ( 1st ` ( h ` ( i + 1 ) ) )
114	113, 11	cfv 5578	. . . . . . . . . . . . . . . 16 class ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
115	109, 114	wceq 1383	. . . . . . . . . . . . . . 15 wff ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
116		cmin 9810	. . . . . . . . . . . . . . . . 17 class -
117	98, 89, 116	co 6281	. . . . . . . . . . . . . . . 16 class ( n - 1 )
118		cfz 11682	. . . . . . . . . . . . . . . 16 class ...
119	89, 117, 118	co 6281	. . . . . . . . . . . . . . 15 class ( 1 ... ( n - 1 ) )
120	115, 105, 119	wral 2793	. . . . . . . . . . . . . 14 wff A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
121	97, 104, 120	w3a 974	. . . . . . . . . . . . 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 ) ) ) ) )
122	17, 17	cxp 4987	. . . . . . . . . . . . . 14 class ( v X. v )
123	89, 98, 118	co 6281	. . . . . . . . . . . . . 14 class ( 1 ... n )
124		cmap 7422	. . . . . . . . . . . . . 14 class ^m
125	122, 123, 124	co 6281	. . . . . . . . . . . . 13 class ( ( v X. v ) ^m ( 1 ... n ) )
126	121, 90, 125	crab 2797	. . . . . . . . . . . 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 14878	. . . . . . . . . . . . 13 class RR*s
128	6, 83	cfv 5578	. . . . . . . . . . . . . 14 class ( dist ` r )
129	88	cv 1382	. . . . . . . . . . . . . 14 class g
130	128, 129	ccom 4993	. . . . . . . . . . . . 13 class ( ( dist ` r ) o. g )
131		cgsu 14819	. . . . . . . . . . . . 13 class gsumg
132	127, 130, 131	co 6281	. . . . . . . . . . . 12 class ( RR*s gsumg ( ( dist ` r ) o. g ) )
133	88, 126, 132	cmpt 4495	. . . . . . . . . . 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 ) ) )
134	133	crn 4990	. . . . . . . . . 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 ) ) )
135	86, 87, 134	ciun 4315	. . . . . . . . 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 9630	. . . . . . . . 9 class RR*
137		clt 9631	. . . . . . . . . 10 class <
138	137	ccnv 4988	. . . . . . . . 9 class `' <
139	135, 136, 138	csup 7902	. . . . . . . 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* , `' < )
140	49, 85, 12, 12, 139	cmpt2 6283	. . . . . . 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* , `' < ) )
141	84, 140	cop 4020	. . . . . 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* , `' < ) ) >.
142	75, 82, 141	ctp 4018	. . . . 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* , `' < ) ) >. }
143	68, 142	cun 3459	. . . 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* , `' < ) ) >. } )
144	5, 8, 143	csb 3420	. . 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* , `' < ) ) >. } )
145	2, 3, 4, 4, 144	cmpt2 6283	. 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* , `' < ) ) >. } ) )
146	1, 145	wceq 1383	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* , `' < ) ) >. } ) )

This definition is referenced by:  imasval  14889