Definition df-imas 15485

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

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 |-> 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 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 15480	. 2 class "s
2		vf	. . 3 setvar f
3		vr	. . 3 setvar r
4		cvv 3031	. . 3 class _V
5		vv	. . . 4 setvar v
6	3	cv 1451	. . . . 5 class r
7		cbs 15199	. . . . 5 class Base
8	6, 7	cfv 5589	. . . 4 class ( Base ` r )
9		cnx 15196	. . . . . . . . 9 class ndx
10	9, 7	cfv 5589	. . . . . . . 8 class ( Base ` ndx )
11	2	cv 1451	. . . . . . . . 9 class f
12	11	crn 4840	. . . . . . . 8 class ran f
13	10, 12	cop 3965	. . . . . . 7 class <. ( Base ` ndx ) , ran f >.
14		cplusg 15268	. . . . . . . . 9 class +g
15	9, 14	cfv 5589	. . . . . . . 8 class ( +g ` ndx )
16		vp	. . . . . . . . 9 setvar p
17	5	cv 1451	. . . . . . . . 9 class v
18		vq	. . . . . . . . . 10 setvar q
19	16	cv 1451	. . . . . . . . . . . . . 14 class p
20	19, 11	cfv 5589	. . . . . . . . . . . . 13 class ( f ` p )
21	18	cv 1451	. . . . . . . . . . . . . 14 class q
22	21, 11	cfv 5589	. . . . . . . . . . . . 13 class ( f ` q )
23	20, 22	cop 3965	. . . . . . . . . . . 12 class <. ( f ` p ) , ( f ` q ) >.
24	6, 14	cfv 5589	. . . . . . . . . . . . . 14 class ( +g ` r )
25	19, 21, 24	co 6308	. . . . . . . . . . . . 13 class ( p ( +g ` r ) q )
26	25, 11	cfv 5589	. . . . . . . . . . . 12 class ( f ` ( p ( +g ` r ) q ) )
27	23, 26	cop 3965	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >.
28	27	csn 3959	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
29	18, 17, 28	ciun 4269	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
30	16, 17, 29	ciun 4269	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
31	15, 30	cop 3965	. . . . . . 7 class <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >.
32		cmulr 15269	. . . . . . . . 9 class .r
33	9, 32	cfv 5589	. . . . . . . 8 class ( .r ` ndx )
34	6, 32	cfv 5589	. . . . . . . . . . . . . 14 class ( .r ` r )
35	19, 21, 34	co 6308	. . . . . . . . . . . . 13 class ( p ( .r ` r ) q )
36	35, 11	cfv 5589	. . . . . . . . . . . 12 class ( f ` ( p ( .r ` r ) q ) )
37	23, 36	cop 3965	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >.
38	37	csn 3959	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
39	18, 17, 38	ciun 4269	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
40	16, 17, 39	ciun 4269	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
41	33, 40	cop 3965	. . . . . . 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 3963	. . . . . 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 15271	. . . . . . . . 9 class Scalar
44	9, 43	cfv 5589	. . . . . . . 8 class (Scalar ` ndx )
45	6, 43	cfv 5589	. . . . . . . 8 class (Scalar ` r )
46	44, 45	cop 3965	. . . . . . 7 class <. (Scalar ` ndx ) , (Scalar ` r ) >.
47		cvsca 15272	. . . . . . . . 9 class .s
48	9, 47	cfv 5589	. . . . . . . 8 class ( .s ` ndx )
49		vx	. . . . . . . . . 10 setvar x
50	45, 7	cfv 5589	. . . . . . . . . 10 class ( Base ` (Scalar ` r ) )
51	22	csn 3959	. . . . . . . . . 10 class { ( f ` q ) }
52	6, 47	cfv 5589	. . . . . . . . . . . 12 class ( .s ` r )
53	19, 21, 52	co 6308	. . . . . . . . . . 11 class ( p ( .s ` r ) q )
54	53, 11	cfv 5589	. . . . . . . . . 10 class ( f ` ( p ( .s ` r ) q ) )
55	16, 49, 50, 51, 54	cmpt2 6310	. . . . . . . . 9 class ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
56	18, 17, 55	ciun 4269	. . . . . . . 8 class U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) )
57	48, 56	cop 3965	. . . . . . 7 class <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >.
58		cip 15273	. . . . . . . . 9 class .i
59	9, 58	cfv 5589	. . . . . . . 8 class ( .i ` ndx )
60	6, 58	cfv 5589	. . . . . . . . . . . . 13 class ( .i ` r )
61	19, 21, 60	co 6308	. . . . . . . . . . . 12 class ( p ( .i ` r ) q )
62	23, 61	cop 3965	. . . . . . . . . . 11 class <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >.
63	62	csn 3959	. . . . . . . . . 10 class { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
64	18, 17, 63	ciun 4269	. . . . . . . . 9 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
65	16, 17, 64	ciun 4269	. . . . . . . 8 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. }
66	59, 65	cop 3965	. . . . . . 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 3963	. . . . . 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 3388	. . . . 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 15274	. . . . . . . 8 class TopSet
70	9, 69	cfv 5589	. . . . . . 7 class (TopSet ` ndx )
71		ctopn 15398	. . . . . . . . 9 class TopOpen
72	6, 71	cfv 5589	. . . . . . . 8 class ( TopOpen ` r )
73		cqtop 15479	. . . . . . . 8 class qTop
74	72, 11, 73	co 6308	. . . . . . 7 class ( ( TopOpen ` r ) qTop f )
75	70, 74	cop 3965	. . . . . 6 class <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >.
76		cple 15275	. . . . . . . 8 class le
77	9, 76	cfv 5589	. . . . . . 7 class ( le ` ndx )
78	6, 76	cfv 5589	. . . . . . . . 9 class ( le ` r )
79	11, 78	ccom 4843	. . . . . . . 8 class ( f o. ( le ` r ) )
80	11	ccnv 4838	. . . . . . . 8 class `' f
81	79, 80	ccom 4843	. . . . . . 7 class ( ( f o. ( le ` r ) ) o. `' f )
82	77, 81	cop 3965	. . . . . 6 class <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >.
83		cds 15277	. . . . . . . 8 class dist
84	9, 83	cfv 5589	. . . . . . 7 class ( dist ` ndx )
85		vy	. . . . . . . 8 setvar y
86		vn	. . . . . . . . . 10 setvar n
87		cn 10631	. . . . . . . . . 10 class NN
88		vg	. . . . . . . . . . . 12 setvar g
89		c1 9558	. . . . . . . . . . . . . . . . . 18 class 1
90		vh	. . . . . . . . . . . . . . . . . . 19 setvar h
91	90	cv 1451	. . . . . . . . . . . . . . . . . 18 class h
92	89, 91	cfv 5589	. . . . . . . . . . . . . . . . 17 class ( h ` 1 )
93		c1st 6810	. . . . . . . . . . . . . . . . 17 class 1st
94	92, 93	cfv 5589	. . . . . . . . . . . . . . . 16 class ( 1st ` ( h ` 1 ) )
95	94, 11	cfv 5589	. . . . . . . . . . . . . . 15 class ( f ` ( 1st ` ( h ` 1 ) ) )
96	49	cv 1451	. . . . . . . . . . . . . . 15 class x
97	95, 96	wceq 1452	. . . . . . . . . . . . . 14 wff ( f ` ( 1st ` ( h ` 1 ) ) ) = x
98	86	cv 1451	. . . . . . . . . . . . . . . . . 18 class n
99	98, 91	cfv 5589	. . . . . . . . . . . . . . . . 17 class ( h ` n )
100		c2nd 6811	. . . . . . . . . . . . . . . . 17 class 2nd
101	99, 100	cfv 5589	. . . . . . . . . . . . . . . 16 class ( 2nd ` ( h ` n ) )
102	101, 11	cfv 5589	. . . . . . . . . . . . . . 15 class ( f ` ( 2nd ` ( h ` n ) ) )
103	85	cv 1451	. . . . . . . . . . . . . . 15 class y
104	102, 103	wceq 1452	. . . . . . . . . . . . . 14 wff ( f ` ( 2nd ` ( h ` n ) ) ) = y
105		vi	. . . . . . . . . . . . . . . . . . . 20 setvar i
106	105	cv 1451	. . . . . . . . . . . . . . . . . . 19 class i
107	106, 91	cfv 5589	. . . . . . . . . . . . . . . . . 18 class ( h ` i )
108	107, 100	cfv 5589	. . . . . . . . . . . . . . . . 17 class ( 2nd ` ( h ` i ) )
109	108, 11	cfv 5589	. . . . . . . . . . . . . . . 16 class ( f ` ( 2nd ` ( h ` i ) ) )
110		caddc 9560	. . . . . . . . . . . . . . . . . . . 20 class +
111	106, 89, 110	co 6308	. . . . . . . . . . . . . . . . . . 19 class ( i + 1 )
112	111, 91	cfv 5589	. . . . . . . . . . . . . . . . . 18 class ( h ` ( i + 1 ) )
113	112, 93	cfv 5589	. . . . . . . . . . . . . . . . 17 class ( 1st ` ( h ` ( i + 1 ) ) )
114	113, 11	cfv 5589	. . . . . . . . . . . . . . . 16 class ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
115	109, 114	wceq 1452	. . . . . . . . . . . . . . 15 wff ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
116		cmin 9880	. . . . . . . . . . . . . . . . 17 class -
117	98, 89, 116	co 6308	. . . . . . . . . . . . . . . 16 class ( n - 1 )
118		cfz 11810	. . . . . . . . . . . . . . . 16 class ...
119	89, 117, 118	co 6308	. . . . . . . . . . . . . . 15 class ( 1 ... ( n - 1 ) )
120	115, 105, 119	wral 2756	. . . . . . . . . . . . . 14 wff A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) )
121	97, 104, 120	w3a 1007	. . . . . . . . . . . . 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 4837	. . . . . . . . . . . . . 14 class ( v X. v )
123	89, 98, 118	co 6308	. . . . . . . . . . . . . 14 class ( 1 ... n )
124		cmap 7490	. . . . . . . . . . . . . 14 class ^m
125	122, 123, 124	co 6308	. . . . . . . . . . . . 13 class ( ( v X. v ) ^m ( 1 ... n ) )
126	121, 90, 125	crab 2760	. . . . . . . . . . . 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 15476	. . . . . . . . . . . . 13 class RR*s
128	6, 83	cfv 5589	. . . . . . . . . . . . . 14 class ( dist ` r )
129	88	cv 1451	. . . . . . . . . . . . . 14 class g
130	128, 129	ccom 4843	. . . . . . . . . . . . 13 class ( ( dist ` r ) o. g )
131		cgsu 15417	. . . . . . . . . . . . 13 class gsumg
132	127, 130, 131	co 6308	. . . . . . . . . . . 12 class ( RR*s gsumg ( ( dist ` r ) o. g ) )
133	88, 126, 132	cmpt 4454	. . . . . . . . . . 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 4840	. . . . . . . . . 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 4269	. . . . . . . . 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 9692	. . . . . . . . 9 class RR*
137		clt 9693	. . . . . . . . 9 class <
138	135, 136, 137	cinf 7973	. . . . . . . 8 class 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < )
139	49, 85, 12, 12, 138	cmpt2 6310	. . . . . . 7 class ( 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) )
140	84, 139	cop 3965	. . . . . 6 class <. ( 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >.
141	75, 82, 140	ctp 3963	. . . . 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 |-> 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. }
142	68, 141	cun 3388	. . . 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 |-> 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } )
143	5, 8, 142	csb 3349	. . 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 |-> 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } )
144	2, 3, 4, 4, 143	cmpt2 6310	. 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 |-> 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )
145	1, 144	wceq 1452	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 |-> 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 gsumg ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )

This definition is referenced by:  imasval  15489