Definition 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 = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( .r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1st ‘ 𝑎 ) 𝑥 ( 2nd ‘ 𝑏 ) ) ( -g ‘ 𝑟 ) ( ( 1st ‘ 𝑏 ) 𝑥 ( 2nd ‘ 𝑎 ) ) ) ) = ( 0g ‘ 𝑟 ) ) } )

Detailed syntax breakdown

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