This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑟 ) ) } )