Definition df-erl 33255

Description: Define the operation giving the equivalence relation used in the localization of a ring 𝑟 by a set 𝑠. Two pairs 𝑎 = ⟨𝑥, 𝑦⟩ and 𝑏 = ⟨𝑧, 𝑤⟩ are equivalent if there exists 𝑡 ∈ 𝑠 such that 𝑡 · (𝑥 · 𝑤 − 𝑧 · 𝑦) = 0. This corresponds to the usual comparison of fractions 𝑥 / 𝑦 and 𝑧 / 𝑤. (Contributed by Thierry Arnoux, 28-Apr-2025.)

Assertion

Ref	Expression
df-erl	⊢ ~RL = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))})

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

Detailed syntax breakdown of Definition df-erl

Step	Hyp	Ref	Expression
1		cerl 33253	. 2 class ~RL
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3464	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1539	. . . . 5 class 𝑟
7		cmulr 17277	. . . . 5 class .r
8	6, 7	cfv 6536	. . . 4 class (.r‘𝑟)
9		vw	. . . . 5 setvar 𝑤
10		cbs 17233	. . . . . . 7 class Base
11	6, 10	cfv 6536	. . . . . 6 class (Base‘𝑟)
12	3	cv 1539	. . . . . 6 class 𝑠
13	11, 12	cxp 5657	. . . . 5 class ((Base‘𝑟) × 𝑠)
14		va	. . . . . . . . 9 setvar 𝑎
15	14, 9	wel 2110	. . . . . . . 8 wff 𝑎 ∈ 𝑤
16		vb	. . . . . . . . 9 setvar 𝑏
17	16, 9	wel 2110	. . . . . . . 8 wff 𝑏 ∈ 𝑤
18	15, 17	wa 395	. . . . . . 7 wff (𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤)
19		vt	. . . . . . . . . . 11 setvar 𝑡
20	19	cv 1539	. . . . . . . . . 10 class 𝑡
21	14	cv 1539	. . . . . . . . . . . . 13 class 𝑎
22		c1st 7991	. . . . . . . . . . . . 13 class 1st
23	21, 22	cfv 6536	. . . . . . . . . . . 12 class (1st ‘𝑎)
24	16	cv 1539	. . . . . . . . . . . . 13 class 𝑏
25		c2nd 7992	. . . . . . . . . . . . 13 class 2nd
26	24, 25	cfv 6536	. . . . . . . . . . . 12 class (2nd ‘𝑏)
27	5	cv 1539	. . . . . . . . . . . 12 class 𝑥
28	23, 26, 27	co 7410	. . . . . . . . . . 11 class ((1st ‘𝑎)𝑥(2nd ‘𝑏))
29	24, 22	cfv 6536	. . . . . . . . . . . 12 class (1st ‘𝑏)
30	21, 25	cfv 6536	. . . . . . . . . . . 12 class (2nd ‘𝑎)
31	29, 30, 27	co 7410	. . . . . . . . . . 11 class ((1st ‘𝑏)𝑥(2nd ‘𝑎))
32		csg 18923	. . . . . . . . . . . 12 class -g
33	6, 32	cfv 6536	. . . . . . . . . . 11 class (-g‘𝑟)
34	28, 31, 33	co 7410	. . . . . . . . . 10 class (((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))
35	20, 34, 27	co 7410	. . . . . . . . 9 class (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))
36		c0g 17458	. . . . . . . . . 10 class 0g
37	6, 36	cfv 6536	. . . . . . . . 9 class (0g‘𝑟)
38	35, 37	wceq 1540	. . . . . . . 8 wff (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟)
39	38, 19, 12	wrex 3061	. . . . . . 7 wff ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟)
40	18, 39	wa 395	. . . . . 6 wff ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))
41	40, 14, 16	copab 5186	. . . . 5 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))}
42	9, 13, 41	csb 3879	. . . 4 class ⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))}
43	5, 8, 42	csb 3879	. . 3 class ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))}
44	2, 3, 4, 4, 43	cmpo 7412	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))})
45	1, 44	wceq 1540	1 wff ~RL = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))})

This definition is referenced by:  erlval  33258