df-erl

Description: Define the operation giving the equivalence relation used in the localization of a ring r by a set s . Two pairs a = <. x , y >. and b = <. z , w >. are equivalent if there exists t e. s such that t x. ( x x. w - z x. y ) = 0 . This corresponds to the usual comparison of fractions x / y and z / w . (Contributed by Thierry Arnoux, 28-Apr-2025)

		Ref	Expression
	Assertion	df-erl	$⊢ ~_{RL} = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cerl	$class ~_{RL}$
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		va	$setvar a$
14		vb	$setvar b$
15	13	cv	$setvar a$
16	12	cv	$setvar w$
17	15 16	wcel	$wff a \in w$
18	14	cv	$setvar b$
19	18 16	wcel	$wff b \in w$
20	17 19	wa	$wff (a \in w \land b \in w)$
21		vt	$setvar t$
22	21	cv	$setvar t$
23	7	cv	$setvar x$
24		c1st	$class 1^{st}$
25	15 24	cfv	$class 1^{st} (a)$
26		c2nd	$class 2^{nd}$
27	18 26	cfv	$class 2^{nd} (b)$
28	25 27 23	co	$class (1^{st} (a) x 2^{nd} (b))$
29		csg	$class -_{𝑔}$
30	5 29	cfv	$class -_{r}$
31	18 24	cfv	$class 1^{st} (b)$
32	15 26	cfv	$class 2^{nd} (a)$
33	31 32 23	co	$class (1^{st} (b) x 2^{nd} (a))$
34	28 33 30	co	$class ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a)))$
35	22 34 23	co	$class (t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))))$
36		c0g	$class 0_{𝑔}$
37	5 36	cfv	$class 0_{r}$
38	35 37	wceq	$wff t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r}$
39	38 21 10	wrex	$wff \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r}$
40	20 39	wa	$wff ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})$
41	40 13 14	copab	$class \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\}$
42	12 11 41	csb	$class ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\}$
43	7 6 42	csb	$class ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\}$
44	1 3 2 2 43	cmpo	$class (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\})$
45	0 44	wceq	$wff ~_{RL} = (r \in V, s \in V ⟼ ⦋ \cdot_{r} / x ⦌ ⦋ ({Base}_{r} \times s) / w ⦌ \{⟨a, b⟩ \| ((a \in w \land b \in w) \land \exists t \in s t x ((1^{st} (a) x 2^{nd} (b)) -_{r} (1^{st} (b) x 2^{nd} (a))) = 0_{r})\})$

Metamath Proof Explorer

Definition df-erl

Detailed syntax breakdown