Definition df-imas

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 , 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 ) and/or R ( with df-ress ) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by AV, 6-Oct-2020)

	Ref	Expression
Assertion	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 |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimas	|- "s
1		vf	|- f
2		cvv	|- _V
3		vr	|- r
4		cbs	|- Base
5	3	cv	|- r
6	5 4	cfv	|- ( Base ` r )
7		vv	|- v
8		cnx	|- ndx
9	8 4	cfv	|- ( Base ` ndx )
10	1	cv	|- f
11	10	crn	|- ran f
12	9 11	cop	|- <. ( Base ` ndx ) , ran f >.
13		cplusg	|- +g
14	8 13	cfv	|- ( +g ` ndx )
15		vp	|- p
16	7	cv	|- v
17		vq	|- q
18	15	cv	|- p
19	18 10	cfv	|- ( f ` p )
20	17	cv	|- q
21	20 10	cfv	|- ( f ` q )
22	19 21	cop	|- <. ( f ` p ) , ( f ` q ) >.
23	5 13	cfv	|- ( +g ` r )
24	18 20 23	co	|- ( p ( +g ` r ) q )
25	24 10	cfv	|- ( f ` ( p ( +g ` r ) q ) )
26	22 25	cop	|- <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >.
27	26	csn	|- { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
28	17 16 27	ciun	|- U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
29	15 16 28	ciun	|- U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
30	14 29	cop	|- <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >.
31		cmulr	|- .r
32	8 31	cfv	|- ( .r ` ndx )
33	5 31	cfv	|- ( .r ` r )
34	18 20 33	co	|- ( p ( .r ` r ) q )
35	34 10	cfv	|- ( f ` ( p ( .r ` r ) q ) )
36	22 35	cop	|- <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >.
37	36	csn	|- { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
38	17 16 37	ciun	|- U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
39	15 16 38	ciun	|- U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
40	32 39	cop	|- <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >.
41	12 30 40	ctp	|- { <. ( 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 ) ) >. } >. }
42		csca	|- Scalar
43	8 42	cfv	|- ( Scalar ` ndx )
44	5 42	cfv	|- ( Scalar ` r )
45	43 44	cop	|- <. ( Scalar ` ndx ) , ( Scalar ` r ) >.
46		cvsca	|- .s
47	8 46	cfv	|- ( .s ` ndx )
48	44 4	cfv	|- ( Base ` ( Scalar ` r ) )
49		vx	|- x
50	21	csn	|- { ( f ` q ) }
51	5 46	cfv	|- ( .s ` r )
52	18 20 51	co	|- ( p ( .s ` r ) q )
53	52 10	cfv	|- ( f ` ( p ( .s ` r ) q ) )
54	15 49 48 50 53	cmpo	|- ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
55	17 16 54	ciun	|- U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
56	47 55	cop	|- <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >.
57		cip	|- .i
58	8 57	cfv	|- ( .i ` ndx )
59	5 57	cfv	|- ( .i ` r )
60	18 20 59	co	|- ( p ( .i ` r ) q )
61	22 60	cop	|- <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >.
62	61	csn	|- { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
63	17 16 62	ciun	|- U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
64	15 16 63	ciun	|- U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
65	58 64	cop	|- <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >.
66	45 56 65	ctp	|- { <. ( 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 ) >. } >. }
67	41 66	cun	|- ( { <. ( 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 ) >. } >. } )
68		cts	|- TopSet
69	8 68	cfv	|- ( TopSet ` ndx )
70		ctopn	|- TopOpen
71	5 70	cfv	|- ( TopOpen ` r )
72		cqtop	|- qTop
73	71 10 72	co	|- ( ( TopOpen ` r ) qTop f )
74	69 73	cop	|- <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >.
75		cple	|- le
76	8 75	cfv	|- ( le ` ndx )
77	5 75	cfv	|- ( le ` r )
78	10 77	ccom	|- ( f o. ( le ` r ) )
79	10	ccnv	|- `' f
80	78 79	ccom	|- ( ( f o. ( le ` r ) ) o. `' f )
81	76 80	cop	|- <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >.
82		cds	|- dist
83	8 82	cfv	|- ( dist ` ndx )
84		vy	|- y
85		vn	|- n
86		cn	|- NN
87		vg	|- g
88		vh	|- h
89	16 16	cxp	|- ( v X. v )
90		cmap	|- ^m
91		c1	|- 1
92		cfz	|- ...
93	85	cv	|- n
94	91 93 92	co	|- ( 1 ... n )
95	89 94 90	co	|- ( ( v X. v ) ^m ( 1 ... n ) )
96		c1st	|- 1st
97	88	cv	|- h
98	91 97	cfv	|- ( h ` 1 )
99	98 96	cfv	|- ( 1st ` ( h ` 1 ) )
100	99 10	cfv	|- ( f ` ( 1st ` ( h ` 1 ) ) )
101	49	cv	|- x
102	100 101	wceq	|- ( f ` ( 1st ` ( h ` 1 ) ) ) = x
103		c2nd	|- 2nd
104	93 97	cfv	|- ( h ` n )
105	104 103	cfv	|- ( 2nd ` ( h ` n ) )
106	105 10	cfv	|- ( f ` ( 2nd ` ( h ` n ) ) )
107	84	cv	|- y
108	106 107	wceq	|- ( f ` ( 2nd ` ( h ` n ) ) ) = y
109		vi	|- i
110		cmin	|- -
111	93 91 110	co	|- ( n - 1 )
112	91 111 92	co	|- ( 1 ... ( n - 1 ) )
113	109	cv	|- i
114	113 97	cfv	|- ( h ` i )
115	114 103	cfv	|- ( 2nd ` ( h ` i ) )
116	115 10	cfv	|- ( f ` ( 2nd ` ( h ` i ) ) )
117		caddc	|- +
118	113 91 117	co	|- ( i + 1 )
119	118 97	cfv	|- ( h ` ( i + 1 ) )
120	119 96	cfv	|- ( 1st ` ( h ` ( i + 1 ) ) )
121	120 10	cfv	|- ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
122	116 121	wceq	|- ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
123	122 109 112	wral	|- A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
124	102 108 123	w3a	|- ( ( 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 ) ) ) ) )
125	124 88 95	crab	|- { 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 ) ) ) ) ) }
126		cxrs	|- RR*s
127		cgsu	|- gsum
128	5 82	cfv	|- ( dist ` r )
129	87	cv	|- g
130	128 129	ccom	|- ( ( dist ` r ) o. g )
131	126 130 127	co	|- ( RR*s gsum ( ( dist ` r ) o. g ) )
132	87 125 131	cmpt	|- ( 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 gsum ( ( dist ` r ) o. g ) ) )
133	132	crn	|- 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 gsum ( ( dist ` r ) o. g ) ) )
134	85 86 133	ciun	|- 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 gsum ( ( dist ` r ) o. g ) ) )
135		cxr	|- RR*
136		clt	|- <
137	134 135 136	cinf	|- inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < )
138	49 84 11 11 137	cmpo	|- ( x e. ran f , y e. ran f |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) )
139	83 138	cop	|- <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >.
140	74 81 139	ctp	|- { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. }
141	67 140	cun	|- ( ( { <. ( 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 |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } )
142	7 6 141	csb	|- [_ ( 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 |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } )
143	1 3 2 2 142	cmpo	|- ( 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 |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )
144	0 143	wceq	|- "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 |-> inf ( 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 gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )