Metamath Proof Explorer

Definition df-rloc

Description: Define the operation giving the localization of a ring r by a given set s . The localized ring r RLocal s is the set of equivalence classes of pairs of elements in r over the relation r ~RL s with addition and multiplication defined naturally. (Contributed by Thierry Arnoux, 27-Apr-2025)

Ref Expression
Assertion df-rloc 
|- RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crloc 
 |-  RLocal
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 cnx 
 |-  ndx
14 13 8 cfv 
 |-  ( Base ` ndx )
15 12 cv 
 |-  w
16 14 15 cop 
 |-  <. ( Base ` ndx ) , w >.
17 cplusg 
 |-  +g
18 13 17 cfv 
 |-  ( +g ` ndx )
19 va 
 |-  a
20 vb 
 |-  b
21 c1st 
 |-  1st
22 19 cv 
 |-  a
23 22 21 cfv 
 |-  ( 1st ` a )
24 7 cv 
 |-  x
25 c2nd 
 |-  2nd
26 20 cv 
 |-  b
27 26 25 cfv 
 |-  ( 2nd ` b )
28 23 27 24 co 
 |-  ( ( 1st ` a ) x ( 2nd ` b ) )
29 5 17 cfv 
 |-  ( +g ` r )
30 26 21 cfv 
 |-  ( 1st ` b )
31 22 25 cfv 
 |-  ( 2nd ` a )
32 30 31 24 co 
 |-  ( ( 1st ` b ) x ( 2nd ` a ) )
33 28 32 29 co 
 |-  ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) )
34 31 27 24 co 
 |-  ( ( 2nd ` a ) x ( 2nd ` b ) )
35 33 34 cop 
 |-  <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >.
36 19 20 15 15 35 cmpo 
 |-  ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. )
37 18 36 cop 
 |-  <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >.
38 13 4 cfv 
 |-  ( .r ` ndx )
39 23 30 24 co 
 |-  ( ( 1st ` a ) x ( 1st ` b ) )
40 39 34 cop 
 |-  <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >.
41 19 20 15 15 40 cmpo 
 |-  ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. )
42 38 41 cop 
 |-  <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >.
43 16 37 42 ctp 
 |-  { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. }
44 csca 
 |-  Scalar
45 13 44 cfv 
 |-  ( Scalar ` ndx )
46 5 44 cfv 
 |-  ( Scalar ` r )
47 45 46 cop 
 |-  <. ( Scalar ` ndx ) , ( Scalar ` r ) >.
48 cvsca 
 |-  .s
49 13 48 cfv 
 |-  ( .s ` ndx )
50 vk 
 |-  k
51 46 8 cfv 
 |-  ( Base ` ( Scalar ` r ) )
52 50 cv 
 |-  k
53 5 48 cfv 
 |-  ( .s ` r )
54 52 23 53 co 
 |-  ( k ( .s ` r ) ( 1st ` a ) )
55 54 31 cop 
 |-  <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >.
56 50 19 51 15 55 cmpo 
 |-  ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. )
57 49 56 cop 
 |-  <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >.
58 cip 
 |-  .i
59 13 58 cfv 
 |-  ( .i ` ndx )
60 c0 
 |-  (/)
61 59 60 cop 
 |-  <. ( .i ` ndx ) , (/) >.
62 47 57 61 ctp 
 |-  { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. }
63 43 62 cun 
 |-  ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } )
64 cts 
 |-  TopSet
65 13 64 cfv 
 |-  ( TopSet ` ndx )
66 5 64 cfv 
 |-  ( TopSet ` r )
67 ctx 
 |-  tX
68 crest 
 |-  |`t
69 66 10 68 co 
 |-  ( ( TopSet ` r ) |`t s )
70 66 69 67 co 
 |-  ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) )
71 65 70 cop 
 |-  <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >.
72 cple 
 |-  le
73 13 72 cfv 
 |-  ( le ` ndx )
74 22 15 wcel 
 |-  a e. w
75 26 15 wcel 
 |-  b e. w
76 74 75 wa 
 |-  ( a e. w /\ b e. w )
77 5 72 cfv 
 |-  ( le ` r )
78 28 32 77 wbr 
 |-  ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) )
79 76 78 wa 
 |-  ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) )
80 79 19 20 copab 
 |-  { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) }
81 73 80 cop 
 |-  <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >.
82 cds 
 |-  dist
83 13 82 cfv 
 |-  ( dist ` ndx )
84 5 82 cfv 
 |-  ( dist ` r )
85 28 32 84 co 
 |-  ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) )
86 19 20 15 15 85 cmpo 
 |-  ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) )
87 83 86 cop 
 |-  <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >.
88 71 81 87 ctp 
 |-  { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. }
89 63 88 cun 
 |-  ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } )
90 cqus 
 |-  /s
91 cerl 
 |-  ~RL
92 5 10 91 co 
 |-  ( r ~RL s )
93 89 92 90 co 
 |-  ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) )
94 12 11 93 csb 
 |-  [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) )
95 7 6 94 csb 
 |-  [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) )
96 1 3 2 2 95 cmpo 
 |-  ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) )
97 0 96 wceq 
 |-  RLocal = ( r e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) )