Definition df-rloc 33817

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

Assertion

Ref

Expression

df-rloc

⊢ RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))

Distinct variable group:   𝑠,𝑟,𝑥,𝑤,𝑎,𝑏,𝑘

Detailed syntax breakdown of Definition df-rloc

Step	Hyp	Ref	Expression
1		crloc 33815	. 2 class RLocal
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3451	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1569	. . . . 5 class 𝑟
7		cmulr 17429	. . . . 5 class .r
8	6, 7	cfv 6538	. . . 4 class (.r‘𝑟)
9		vw	. . . . 5 setvar 𝑤
10		cbs 17387	. . . . . . 7 class Base
11	6, 10	cfv 6538	. . . . . 6 class (Base‘𝑟)
12	3	cv 1569	. . . . . 6 class 𝑠
13	11, 12	cxp 5649	. . . . 5 class ((Base‘𝑟) × 𝑠)
14		cnx 17371	. . . . . . . . . . 11 class ndx
15	14, 10	cfv 6538	. . . . . . . . . 10 class (Base‘ndx)
16	9	cv 1569	. . . . . . . . . 10 class 𝑤
17	15, 16	cop 4590	. . . . . . . . 9 class ⟨(Base‘ndx), 𝑤⟩
18		cplusg 17428	. . . . . . . . . . 11 class +g
19	14, 18	cfv 6538	. . . . . . . . . 10 class (+g‘ndx)
20		va	. . . . . . . . . . 11 setvar 𝑎
21		vb	. . . . . . . . . . 11 setvar 𝑏
22	20	cv 1569	. . . . . . . . . . . . . . 15 class 𝑎
23		c1st 7999	. . . . . . . . . . . . . . 15 class 1st
24	22, 23	cfv 6538	. . . . . . . . . . . . . 14 class (1st ‘𝑎)
25	21	cv 1569	. . . . . . . . . . . . . . 15 class 𝑏
26		c2nd 8000	. . . . . . . . . . . . . . 15 class 2nd
27	25, 26	cfv 6538	. . . . . . . . . . . . . 14 class (2nd ‘𝑏)
28	5	cv 1569	. . . . . . . . . . . . . 14 class 𝑥
29	24, 27, 28	co 7420	. . . . . . . . . . . . 13 class ((1st ‘𝑎)𝑥(2nd ‘𝑏))
30	25, 23	cfv 6538	. . . . . . . . . . . . . 14 class (1st ‘𝑏)
31	22, 26	cfv 6538	. . . . . . . . . . . . . 14 class (2nd ‘𝑎)
32	30, 31, 28	co 7420	. . . . . . . . . . . . 13 class ((1st ‘𝑏)𝑥(2nd ‘𝑎))
33	6, 18	cfv 6538	. . . . . . . . . . . . 13 class (+g‘𝑟)
34	29, 32, 33	co 7420	. . . . . . . . . . . 12 class (((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))
35	31, 27, 28	co 7420	. . . . . . . . . . . 12 class ((2nd ‘𝑎)𝑥(2nd ‘𝑏))
36	34, 35	cop 4590	. . . . . . . . . . 11 class ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩
37	20, 21, 16, 16, 36	cmpo 7422	. . . . . . . . . 10 class (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)
38	19, 37	cop 4590	. . . . . . . . 9 class ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩
39	14, 7	cfv 6538	. . . . . . . . . 10 class (.r‘ndx)
40	24, 30, 28	co 7420	. . . . . . . . . . . 12 class ((1st ‘𝑎)𝑥(1st ‘𝑏))
41	40, 35	cop 4590	. . . . . . . . . . 11 class ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩
42	20, 21, 16, 16, 41	cmpo 7422	. . . . . . . . . 10 class (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)
43	39, 42	cop 4590	. . . . . . . . 9 class ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩
44	17, 38, 43	ctp 4588	. . . . . . . 8 class {⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩}
45		csca 17431	. . . . . . . . . . 11 class Scalar
46	14, 45	cfv 6538	. . . . . . . . . 10 class (Scalar‘ndx)
47	6, 45	cfv 6538	. . . . . . . . . 10 class (Scalar‘𝑟)
48	46, 47	cop 4590	. . . . . . . . 9 class ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩
49		cvsca 17432	. . . . . . . . . . 11 class ·𝑠
50	14, 49	cfv 6538	. . . . . . . . . 10 class ( ·𝑠 ‘ndx)
51		vk	. . . . . . . . . . 11 setvar 𝑘
52	47, 10	cfv 6538	. . . . . . . . . . 11 class (Base‘(Scalar‘𝑟))
53	51	cv 1569	. . . . . . . . . . . . 13 class 𝑘
54	6, 49	cfv 6538	. . . . . . . . . . . . 13 class ( ·𝑠 ‘𝑟)
55	53, 24, 54	co 7420	. . . . . . . . . . . 12 class (𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎))
56	55, 31	cop 4590	. . . . . . . . . . 11 class ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩
57	51, 20, 52, 16, 56	cmpo 7422	. . . . . . . . . 10 class (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)
58	50, 57	cop 4590	. . . . . . . . 9 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩
59		cip 17433	. . . . . . . . . . 11 class ·𝑖
60	14, 59	cfv 6538	. . . . . . . . . 10 class (·𝑖‘ndx)
61		c0 4279	. . . . . . . . . 10 class ∅
62	60, 61	cop 4590	. . . . . . . . 9 class ⟨(·𝑖‘ndx), ∅⟩
63	48, 58, 62	ctp 4588	. . . . . . . 8 class {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}
64	44, 63	cun 3897	. . . . . . 7 class ({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩})
65		cts 17434	. . . . . . . . . 10 class TopSet
66	14, 65	cfv 6538	. . . . . . . . 9 class (TopSet‘ndx)
67	6, 65	cfv 6538	. . . . . . . . . 10 class (TopSet‘𝑟)
68		crest 17591	. . . . . . . . . . 11 class ↾t
69	67, 12, 68	co 7420	. . . . . . . . . 10 class ((TopSet‘𝑟) ↾t 𝑠)
70		ctx 23879	. . . . . . . . . 10 class ×t
71	67, 69, 70	co 7420	. . . . . . . . 9 class ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))
72	66, 71	cop 4590	. . . . . . . 8 class ⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩
73		cple 17435	. . . . . . . . . 10 class le
74	14, 73	cfv 6538	. . . . . . . . 9 class (le‘ndx)
75	20, 9	wel 2146	. . . . . . . . . . . 12 wff 𝑎 ∈ 𝑤
76	21, 9	wel 2146	. . . . . . . . . . . 12 wff 𝑏 ∈ 𝑤
77	75, 76	wa 401	. . . . . . . . . . 11 wff (𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤)
78	6, 73	cfv 6538	. . . . . . . . . . . 12 class (le‘𝑟)
79	29, 32, 78	wbr 5103	. . . . . . . . . . 11 wff ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))
80	77, 79	wa 401	. . . . . . . . . 10 wff ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))
81	80, 20, 21	copab 5167	. . . . . . . . 9 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}
82	74, 81	cop 4590	. . . . . . . 8 class ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩
83		cds 17437	. . . . . . . . . 10 class dist
84	14, 83	cfv 6538	. . . . . . . . 9 class (dist‘ndx)
85	6, 83	cfv 6538	. . . . . . . . . . 11 class (dist‘𝑟)
86	29, 32, 85	co 7420	. . . . . . . . . 10 class (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))
87	20, 21, 16, 16, 86	cmpo 7422	. . . . . . . . 9 class (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))
88	84, 87	cop 4590	. . . . . . . 8 class ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩
89	72, 82, 88	ctp 4588	. . . . . . 7 class {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}
90	64, 89	cun 3897	. . . . . 6 class (({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩})
91		cerl 33814	. . . . . . 7 class ~RL
92	6, 12, 91	co 7420	. . . . . 6 class (𝑟 ~RL 𝑠)
93		cqus 17677	. . . . . 6 class /s
94	90, 92, 93	co 7420	. . . . 5 class ((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠))
95	9, 13, 94	csb 3847	. . . 4 class ⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠))
96	5, 8, 95	csb 3847	. . 3 class ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠))
97	2, 3, 4, 4, 96	cmpo 7422	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))
98	1, 97	wceq 1570	1 wff RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·𝑠 ‘𝑟)(1st ‘𝑎)), (2nd ‘𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))

This definition is used by:  reldmrloc  33818  rlocval  33820