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	$$⊢{“}_{𝑠}=\left(f\in \mathrm{V},r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/v⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimas	$$class{“}_{𝑠}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vr	$$setvarr$$
4		cbs	$$class\mathrm{Base}$$
5	3	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7		vv	$$setvarv$$
8		cnx	$$class\mathrm{ndx}$$
9	8 4	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
10	1	cv	$$setvarf$$
11	10	crn	$$class\mathrm{ran}f$$
12	9 11	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩$$
13		cplusg	$$class{+}_{𝑔}$$
14	8 13	cfv	$$class{+}_{\mathrm{ndx}}$$
15		vp	$$setvarp$$
16	7	cv	$$setvarv$$
17		vq	$$setvarq$$
18	15	cv	$$setvarp$$
19	18 10	cfv	$$classf\left(p\right)$$
20	17	cv	$$setvarq$$
21	20 10	cfv	$$classf\left(q\right)$$
22	19 21	cop	$$class⟨f\left(p\right),f\left(q\right)⟩$$
23	5 13	cfv	$$class{+}_r$$
24	18 20 23	co	$$class\left(p{+}_{r}q\right)$$
25	24 10	cfv	$$classf\left(p{+}_{r}q\right)$$
26	22 25	cop	$$class⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩$$
27	26	csn	$$class\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}$$
28	17 16 27	ciun	$$class\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}$$
29	15 16 28	ciun	$$class\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}$$
30	14 29	cop	$$class⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩$$
31		cmulr	$$class{\cdot }_{𝑟}$$
32	8 31	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
33	5 31	cfv	$$class{\cdot }_r$$
34	18 20 33	co	$$class\left(p{\cdot }_{r}q\right)$$
35	34 10	cfv	$$classf\left(p{\cdot }_{r}q\right)$$
36	22 35	cop	$$class⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩$$
37	36	csn	$$class\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}$$
38	17 16 37	ciun	$$class\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}$$
39	15 16 38	ciun	$$class\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}$$
40	32 39	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩$$
41	12 30 40	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}$$
42		csca	$$class\mathrm{Scalar}$$
43	8 42	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
44	5 42	cfv	$$class\mathrm{Scalar}\left(r\right)$$
45	43 44	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩$$
46		cvsca	$$class{\cdot }_{𝑠}$$
47	8 46	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
48	44 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)}$$
49		vx	$$setvarx$$
50	21	csn	$$class\left\{f\left(q\right)\right\}$$
51	5 46	cfv	$$class{\cdot }_r$$
52	18 20 51	co	$$class\left(p{\cdot }_{r}q\right)$$
53	52 10	cfv	$$classf\left(p{\cdot }_{r}q\right)$$
54	15 49 48 50 53	cmpo	$$class\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)$$
55	17 16 54	ciun	$$class\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)$$
56	47 55	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩$$
57		cip	$$class{\cdot }_{𝑖}$$
58	8 57	cfv	$$class{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
59	5 57	cfv	$$class{\cdot }_{𝑖}\left(r\right)$$
60	18 20 59	co	$$class\left(p{\cdot }_{𝑖}\left(r\right)q\right)$$
61	22 60	cop	$$class⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩$$
62	61	csn	$$class\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}$$
63	17 16 62	ciun	$$class\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}$$
64	15 16 63	ciun	$$class\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}$$
65	58 64	cop	$$class⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩$$
66	45 56 65	ctp	$$class\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}$$
67	41 66	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)$$
68		cts	$$class\mathrm{TopSet}$$
69	8 68	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
70		ctopn	$$class\mathrm{TopOpen}$$
71	5 70	cfv	$$class\mathrm{TopOpen}\left(r\right)$$
72		cqtop	$$class\mathrm{qTop}$$
73	71 10 72	co	$$class\left(\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f\right)$$
74	69 73	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩$$
75		cple	$$class\mathrm{le}$$
76	8 75	cfv	$$class{\le }_{\mathrm{ndx}}$$
77	5 75	cfv	$$class{\le }_r$$
78	10 77	ccom	$$class\left(f\circ {\le }_r\right)$$
79	10	ccnv	$$class{f}^{-1}$$
80	78 79	ccom	$$class\left(\left(f\circ {\le }_r\right)\circ f^{-1}\right)$$
81	76 80	cop	$$class⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩$$
82		cds	$$class\mathrm{dist}$$
83	8 82	cfv	$$class\mathrm{dist}\left(\mathrm{ndx}\right)$$
84		vy	$$setvary$$
85		vn	$$setvarn$$
86		cn	$$class\mathbb{N}$$
87		vg	$$setvarg$$
88		vh	$$setvarh$$
89	16 16	cxp	$$class\left(v\times v\right)$$
90		cmap	$$class{\uparrow }_{𝑚}$$
91		c1	$$class1$$
92		cfz	$$class\dots$$
93	85	cv	$$setvarn$$
94	91 93 92	co	$$class\left(1\dots n\right)$$
95	89 94 90	co	$$class\left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)$$
96		c1st	$$class{1}^{st}$$
97	88	cv	$$setvarh$$
98	91 97	cfv	$$classh\left(1\right)$$
99	98 96	cfv	$$class{1}^{st}\left(h\left(1\right)\right)$$
100	99 10	cfv	$$classf\left(1^{st}\left(h\left(1\right)\right)\right)$$
101	49	cv	$$setvarx$$
102	100 101	wceq	$$wfff\left(1^{st}\left(h\left(1\right)\right)\right)=x$$
103		c2nd	$$class{2}^{nd}$$
104	93 97	cfv	$$classh\left(n\right)$$
105	104 103	cfv	$$class{2}^{nd}\left(h\left(n\right)\right)$$
106	105 10	cfv	$$classf\left(2^{nd}\left(h\left(n\right)\right)\right)$$
107	84	cv	$$setvary$$
108	106 107	wceq	$$wfff\left(2^{nd}\left(h\left(n\right)\right)\right)=y$$
109		vi	$$setvari$$
110		cmin	$$class-$$
111	93 91 110	co	$$class\left(n-1\right)$$
112	91 111 92	co	$$class\left(1\dots n-1\right)$$
113	109	cv	$$setvari$$
114	113 97	cfv	$$classh\left(i\right)$$
115	114 103	cfv	$$class{2}^{nd}\left(h\left(i\right)\right)$$
116	115 10	cfv	$$classf\left(2^{nd}\left(h\left(i\right)\right)\right)$$
117		caddc	$$class+$$
118	113 91 117	co	$$class\left(i+1\right)$$
119	118 97	cfv	$$classh\left(i+1\right)$$
120	119 96	cfv	$$class{1}^{st}\left(h\left(i+1\right)\right)$$
121	120 10	cfv	$$classf\left(1^{st}\left(h\left(i+1\right)\right)\right)$$
122	116 121	wceq	$$wfff\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)$$
123	122 109 112	wral	$$wff\forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)$$
124	102 108 123	w3a	$$wff\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)$$
125	124 88 95	crab	$$class\left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}$$
126		cxrs	$$class{ℝ}_{𝑠}^{*}$$
127		cgsu	$$class{\Sigma }_{𝑔}$$
128	5 82	cfv	$$class\mathrm{dist}\left(r\right)$$
129	87	cv	$$setvarg$$
130	128 129	ccom	$$class\left(\mathrm{dist}\left(r\right)\circ g\right)$$
131	126 130 127	co	$$class\left({\sum }_{{ℝ}_{𝑠}^{*}},\left(\mathrm{dist}\left(r\right)\circ g\right)\right)$$
132	87 125 131	cmpt	$$class\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right)$$
133	132	crn	$$class\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right)$$
134	85 86 133	ciun	$$class\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right)$$
135		cxr	$$class{ℝ}^{*}$$
136		clt	$$class<$$
137	134 135 136	cinf	$$classinf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)$$
138	49 84 11 11 137	cmpo	$$class\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)$$
139	83 138	cop	$$class⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩$$
140	74 81 139	ctp	$$class\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}$$
141	67 140	cun	$$class\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}\right)$$
142	7 6 141	csb	$$class⦋{\mathrm{Base}}_r/v⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}\right)$$
143	1 3 2 2 142	cmpo	$$class\left(f\in \mathrm{V},r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/v⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}\right)\right)$$
144	0 143	wceq	$$wff{“}_{𝑠}=\left(f\in \mathrm{V},r\in \mathrm{V}⟼⦋{\mathrm{Base}}_r/v⦌\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ran}f⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{+}_{r}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,f\left(p{\cdot }_{r}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in v}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},x\in \left\{f\left(q\right)\right\}⟼f\left(p{\cdot }_{r}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in v}\bigcup _{q\in v}\left\{⟨⟨f\left(p\right),f\left(q\right)⟩,p{\cdot }_{𝑖}\left(r\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(r\right)\mathrm{qTop}f⟩,⟨{\le }_{\mathrm{ndx}},\left(f\circ {\le }_r\right)\circ f^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in \mathrm{ran}f,y\in \mathrm{ran}f⟼inf\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(v\times v\right)}^{\left(1\dots n\right)}\right)|\left(f\left(1^{st}\left(h\left(1\right)\right)\right)=x\wedge f\left(2^{nd}\left(h\left(n\right)\right)\right)=y\wedge \forall i\in \left(1\dots n-1\right)f\left(2^{nd}\left(h\left(i\right)\right)\right)=f\left(1^{st}\left(h\left(i+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(r\right)\circ g\right)\right),{ℝ}^{*},<\right)\right)⟩\right\}\right)\right)$$