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 = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cerl 
 |-  ~RL
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cmulr 
 |-  .r
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( .r ` r )
7 vx 
 |-  x
8 cbs 
 |-  Base
9 5 8 cfv 
 |-  ( Base ` r )
10 3 cv 
 |-  s
11 9 10 cxp 
 |-  ( ( Base ` r ) X. s )
12 vw 
 |-  w
13 va 
 |-  a
14 vb 
 |-  b
15 13 cv 
 |-  a
16 12 cv 
 |-  w
17 15 16 wcel 
 |-  a e. w
18 14 cv 
 |-  b
19 18 16 wcel 
 |-  b e. w
20 17 19 wa 
 |-  ( a e. w /\ b e. w )
21 vt 
 |-  t
22 21 cv 
 |-  t
23 7 cv 
 |-  x
24 c1st 
 |-  1st
25 15 24 cfv 
 |-  ( 1st ` a )
26 c2nd 
 |-  2nd
27 18 26 cfv 
 |-  ( 2nd ` b )
28 25 27 23 co 
 |-  ( ( 1st ` a ) x ( 2nd ` b ) )
29 csg 
 |-  -g
30 5 29 cfv 
 |-  ( -g ` r )
31 18 24 cfv 
 |-  ( 1st ` b )
32 15 26 cfv 
 |-  ( 2nd ` a )
33 31 32 23 co 
 |-  ( ( 1st ` b ) x ( 2nd ` a ) )
34 28 33 30 co 
 |-  ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) )
35 22 34 23 co 
 |-  ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) )
36 c0g 
 |-  0g
37 5 36 cfv 
 |-  ( 0g ` r )
38 35 37 wceq 
 |-  ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r )
39 38 21 10 wrex 
 |-  E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r )
40 20 39 wa 
 |-  ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) )
41 40 13 14 copab 
 |-  { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) }
42 12 11 41 csb 
 |-  [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) }
43 7 6 42 csb 
 |-  [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) }
44 1 3 2 2 43 cmpo 
 |-  ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } )
45 0 44 wceq 
 |-  ~RL = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ { <. a , b >. | ( ( a e. w /\ b e. w ) /\ E. t e. s ( t x ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( -g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) = ( 0g ` r ) ) } )