Definition df-rloc

Description: Define the operation giving the localization of a ring r by a given set s . The localized ring r RLocal s is the set of equivalence classes of pairs of elements in r over the relation r ~RL s with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025)

	Ref	Expression
Assertion	df-rloc	Could not format assertion : No typesetting found for |- RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crloc	Could not format RLocal : No typesetting found for class RLocal with typecode class
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cmulr	$$class{\cdot }_{𝑟}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\cdot }_r$$
7		vx	$$setvarx$$
8		cbs	$$class\mathrm{Base}$$
9	5 8	cfv	$$class{\mathrm{Base}}_r$$
10	3	cv	$$setvars$$
11	9 10	cxp	$$class\left({\mathrm{Base}}_r\times s\right)$$
12		vw	$$setvarw$$
13		cnx	$$class\mathrm{ndx}$$
14	13 8	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
15	12	cv	$$setvarw$$
16	14 15	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩$$
17		cplusg	$$class{+}_{𝑔}$$
18	13 17	cfv	$$class{+}_{\mathrm{ndx}}$$
19		va	$$setvara$$
20		vb	$$setvarb$$
21		c1st	$$class{1}^{st}$$
22	19	cv	$$setvara$$
23	22 21	cfv	$$class{1}^{st}\left(a\right)$$
24	7	cv	$$setvarx$$
25		c2nd	$$class{2}^{nd}$$
26	20	cv	$$setvarb$$
27	26 25	cfv	$$class{2}^{nd}\left(b\right)$$
28	23 27 24	co	$$class\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)$$
29	5 17	cfv	$$class{+}_r$$
30	26 21	cfv	$$class{1}^{st}\left(b\right)$$
31	22 25	cfv	$$class{2}^{nd}\left(a\right)$$
32	30 31 24	co	$$class\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)$$
33	28 32 29	co	$$class\left(\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)$$
34	31 27 24	co	$$class\left(2^{nd}\left(a\right)x{2}^{nd}\left(b\right)\right)$$
35	33 34	cop	$$class⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩$$
36	19 20 15 15 35	cmpo	$$class\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)$$
37	18 36	cop	$$class⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩$$
38	13 4	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
39	23 30 24	co	$$class\left(1^{st}\left(a\right)x{1}^{st}\left(b\right)\right)$$
40	39 34	cop	$$class⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩$$
41	19 20 15 15 40	cmpo	$$class\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)$$
42	38 41	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩$$
43	16 37 42	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}$$
44		csca	$$class\mathrm{Scalar}$$
45	13 44	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
46	5 44	cfv	$$class\mathrm{Scalar}\left(r\right)$$
47	45 46	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩$$
48		cvsca	$$class{\cdot }_{𝑠}$$
49	13 48	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
50		vk	$$setvark$$
51	46 8	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)}$$
52	50	cv	$$setvark$$
53	5 48	cfv	$$class{\cdot }_r$$
54	52 23 53	co	$$class\left(k{\cdot }_r{1}^{st}\left(a\right)\right)$$
55	54 31	cop	$$class⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩$$
56	50 19 51 15 55	cmpo	$$class\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)$$
57	49 56	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩$$
58		cip	$$class{\cdot }_{𝑖}$$
59	13 58	cfv	$$class{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
60		c0	$$class\varnothing$$
61	59 60	cop	$$class⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩$$
62	47 57 61	ctp	$$class\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
63	43 62	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)$$
64		cts	$$class\mathrm{TopSet}$$
65	13 64	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
66	5 64	cfv	$$class\mathrm{TopSet}\left(r\right)$$
67		ctx	$$class{\times }_t$$
68		crest	$$class{\upharpoonright }_{𝑡}$$
69	66 10 68	co	$$class\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)$$
70	66 69 67	co	$$class\left(\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)\right)$$
71	65 70	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)⟩$$
72		cple	$$class\mathrm{le}$$
73	13 72	cfv	$$class{\le }_{\mathrm{ndx}}$$
74	22 15	wcel	$$wffa\in w$$
75	26 15	wcel	$$wffb\in w$$
76	74 75	wa	$$wff\left(a\in w\wedge b\in w\right)$$
77	5 72	cfv	$$class{\le }_r$$
78	28 32 77	wbr	$$wff\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)$$
79	76 78	wa	$$wff\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)$$
80	79 19 20	copab	$$class\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}$$
81	73 80	cop	$$class⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}⟩$$
82		cds	$$class\mathrm{dist}$$
83	13 82	cfv	$$class\mathrm{dist}\left(\mathrm{ndx}\right)$$
84	5 82	cfv	$$class\mathrm{dist}\left(r\right)$$
85	28 32 84	co	$$class\left(\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)$$
86	19 20 15 15 85	cmpo	$$class\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)$$
87	83 86	cop	$$class⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)⟩$$
88	71 81 87	ctp	$$class\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)⟩\right\}$$
89	63 88	cun	$$class\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right)$$
90		cqus	$$class{/}_{𝑠}$$
91		cerl	Could not format ~RL : No typesetting found for class ~RL with typecode class
92	5 10 91	co	Could not format ( r ~RL s ) : No typesetting found for class ( r ~RL s ) with typecode class
93	89 92 90	co	Could not format ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) : No typesetting found for class ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) with typecode class
94	12 11 93	csb	Could not format [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) : No typesetting found for class [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) with typecode class
95	7 6 94	csb	Could not format [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) : No typesetting found for class [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) with typecode class
96	1 3 2 2 95	cmpo	Could not format ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) : No typesetting found for class ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) with typecode class
97	0 96	wceq	Could not format RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) : No typesetting found for wff RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) ) with typecode wff