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	$⊢ RLocal = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crloc	$class RLocal$
1		vr	$setvar r$
2		cvv	$class V$
3		vs	$setvar s$
4		cmulr	$class \cdot_{𝑟}$
5	1	cv	$setvar r$
6	5 4	cfv	$class \cdot_{r}$
7		vx	$setvar x$
8		cbs	$class Base$
9	5 8	cfv	$class {Base}_{r}$
10	3	cv	$setvar s$
11	9 10	cxp	$class ({Base}_{r} \times s)$
12		vw	$setvar w$
13		cnx	$class ndx$
14	13 8	cfv	$class {Base}_{ndx}$
15	12	cv	$setvar w$
16	14 15	cop	$class ⟨{Base}_{ndx}, w⟩$
17		cplusg	$class +_{𝑔}$
18	13 17	cfv	$class +_{ndx}$
19		va	$setvar a$
20		vb	$setvar b$
21		c1st	$class 1^{st}$
22	19	cv	$setvar a$
23	22 21	cfv	$class 1^{st} (a)$
24	7	cv	$setvar x$
25		c2nd	$class 2^{nd}$
26	20	cv	$setvar b$
27	26 25	cfv	$class 2^{nd} (b)$
28	23 27 24	co	$class (1^{st} (a) x 2^{nd} (b))$
29	5 17	cfv	$class +_{r}$
30	26 21	cfv	$class 1^{st} (b)$
31	22 25	cfv	$class 2^{nd} (a)$
32	30 31 24	co	$class (1^{st} (b) x 2^{nd} (a))$
33	28 32 29	co	$class ((1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)))$
34	31 27 24	co	$class (2^{nd} (a) x 2^{nd} (b))$
35	33 34	cop	$class ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩$
36	19 20 15 15 35	cmpo	$class (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)$
37	18 36	cop	$class ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩$
38	13 4	cfv	$class \cdot_{ndx}$
39	23 30 24	co	$class (1^{st} (a) x 1^{st} (b))$
40	39 34	cop	$class ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩$
41	19 20 15 15 40	cmpo	$class (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)$
42	38 41	cop	$class ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩$
43	16 37 42	ctp	$class \{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\}$
44		csca	$class Scalar$
45	13 44	cfv	$class Scalar (ndx)$
46	5 44	cfv	$class Scalar (r)$
47	45 46	cop	$class ⟨Scalar (ndx), Scalar (r)⟩$
48		cvsca	$class \cdot_{𝑠}$
49	13 48	cfv	$class \cdot_{ndx}$
50		vk	$setvar k$
51	46 8	cfv	$class {Base}_{Scalar (r)}$
52	50	cv	$setvar k$
53	5 48	cfv	$class \cdot_{r}$
54	52 23 53	co	$class (k \cdot_{r} 1^{st} (a))$
55	54 31	cop	$class ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩$
56	50 19 51 15 55	cmpo	$class (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)$
57	49 56	cop	$class ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩$
58		cip	$class \cdot_{𝑖}$
59	13 58	cfv	$class \cdot_{𝑖} (ndx)$
60		c0	$class \emptyset$
61	59 60	cop	$class ⟨\cdot_{𝑖} (ndx), \emptyset⟩$
62	47 57 61	ctp	$class \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}$
63	43 62	cun	$class (\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\})$
64		cts	$class TopSet$
65	13 64	cfv	$class TopSet (ndx)$
66	5 64	cfv	$class TopSet (r)$
67		ctx	$class \times_{t}$
68		crest	$class ↾_{𝑡}$
69	66 10 68	co	$class (TopSet (r) ↾_{𝑡} s)$
70	66 69 67	co	$class (TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s))$
71	65 70	cop	$class ⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩$
72		cple	$class le$
73	13 72	cfv	$class \leq_{ndx}$
74	22 15	wcel	$wff a \in w$
75	26 15	wcel	$wff b \in w$
76	74 75	wa	$wff (a \in w \land b \in w)$
77	5 72	cfv	$class \leq_{r}$
78	28 32 77	wbr	$wff (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a))$
79	76 78	wa	$wff ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))$
80	79 19 20	copab	$class \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}$
81	73 80	cop	$class ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩$
82		cds	$class dist$
83	13 82	cfv	$class dist (ndx)$
84	5 82	cfv	$class dist (r)$
85	28 32 84	co	$class ((1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))$
86	19 20 15 15 85	cmpo	$class (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))$
87	83 86	cop	$class ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩$
88	71 81 87	ctp	$class \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}$
89	63 88	cun	$class ((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\})$
90		cqus	$class /_{𝑠}$
91		cerl	$class ~_{RL}$
92	5 10 91	co	$class (r ~_{RL} s)$
93	89 92 90	co	$class (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s))$
94	12 11 93	csb	$class ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s))$
95	7 6 94	csb	$class ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s))$
96	1 3 2 2 95	cmpo	$class (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s)))$
97	0 96	wceq	$wff RLocal = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ (((\{⟨{Base}_{ndx}, w⟩, ⟨+_{ndx}, (a \in w, b \in w ⟼ ⟨(1^{st} (a) x 2^{nd} (b)) +_{r} (1^{st} (b) x 2^{nd} (a)), 2^{nd} (a) x 2^{nd} (b)⟩)⟩, ⟨\cdot_{ndx}, (a \in w, b \in w ⟼ ⟨1^{st} (a) x 1^{st} (b), 2^{nd} (a) x 2^{nd} (b)⟩)⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, (k \in {Base}_{Scalar (r)}, a \in w ⟼ ⟨k \cdot_{r} 1^{st} (a), 2^{nd} (a)⟩)⟩, ⟨\cdot_{𝑖} (ndx), \emptyset⟩\}) \cup \{⟨TopSet (ndx), TopSet (r) \times_{t} (TopSet (r) ↾_{𝑡} s)⟩, ⟨\leq_{ndx}, \{⟨a, b⟩ \| ((a \in w \land b \in w) \land (1^{st} (a) x 2^{nd} (b)) \leq_{r} (1^{st} (b) x 2^{nd} (a)))\}⟩, ⟨dist (ndx), (a \in w, b \in w ⟼ (1^{st} (a) x 2^{nd} (b)) dist (r) (1^{st} (b) x 2^{nd} (a)))⟩\}) /_{𝑠} (r ~_{RL} s)))$

Metamath Proof Explorer

Definition df-rloc

Detailed syntax breakdown