Metamath Proof Explorer

Theorem rlocinvunit

Description: In the localization of a ring R at S , inverses of elements of S are units. (Contributed by Thierry Arnoux, 6-Jun-2026)

Ref Expression
Hypotheses rlocinvunit.b 
|- B = ( Base ` R )
rlocinvunit.1 
|- .1. = ( 1r ` R )
rlocinvunit.e 
|- .~ = ( R ~RL S )
rlocinvunit.l 
|- L = ( R RLocal S )
rlocinvunit.w 
|- W = ( Unit ` L )
rlocinvunit.r 
|- ( ph -> R e. CRing )
rlocinvunit.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
rlocinvunit.q 
|- ( ph -> Q e. S )
Assertion rlocinvunit 
|- ( ph -> [ <. .1. , Q >. ] .~ e. W )

Proof

Step Hyp Ref Expression
1 rlocinvunit.b 
 |-  B = ( Base ` R )
2 rlocinvunit.1 
 |-  .1. = ( 1r ` R )
3 rlocinvunit.e 
 |-  .~ = ( R ~RL S )
4 rlocinvunit.l 
 |-  L = ( R RLocal S )
5 rlocinvunit.w 
 |-  W = ( Unit ` L )
6 rlocinvunit.r 
 |-  ( ph -> R e. CRing )
7 rlocinvunit.s 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
8 rlocinvunit.q 
 |-  ( ph -> Q e. S )
9 oveq2 
 |-  ( a = [ <. Q , .1. >. ] .~ -> ( [ <. .1. , Q >. ] .~ ( .r ` L ) a ) = ( [ <. .1. , Q >. ] .~ ( .r ` L ) [ <. Q , .1. >. ] .~ ) )
10 9 eqeq1d 
 |-  ( a = [ <. Q , .1. >. ] .~ -> ( ( [ <. .1. , Q >. ] .~ ( .r ` L ) a ) = ( 1r ` L ) <-> ( [ <. .1. , Q >. ] .~ ( .r ` L ) [ <. Q , .1. >. ] .~ ) = ( 1r ` L ) ) )
11 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
12 11 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
13 12 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
14 7 13 syl 
 |-  ( ph -> S C_ B )
15 14 8 sseldd 
 |-  ( ph -> Q e. B )
16 11 2 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
17 16 subm0cl 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> .1. e. S )
18 7 17 syl 
 |-  ( ph -> .1. e. S )
19 15 18 opelxpd 
 |-  ( ph -> <. Q , .1. >. e. ( B X. S ) )
20 3 ovexi 
 |-  .~ e. _V
21 20 ecelqsi 
 |-  ( <. Q , .1. >. e. ( B X. S ) -> [ <. Q , .1. >. ] .~ e. ( ( B X. S ) /. .~ ) )
22 19 21 syl 
 |-  ( ph -> [ <. Q , .1. >. ] .~ e. ( ( B X. S ) /. .~ ) )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 eqid 
 |-  ( -g ` R ) = ( -g ` R )
26 eqid 
 |-  ( B X. S ) = ( B X. S )
27 1 23 24 25 26 4 3 6 14 rlocbas 
 |-  ( ph -> ( ( B X. S ) /. .~ ) = ( Base ` L ) )
28 22 27 eleqtrd 
 |-  ( ph -> [ <. Q , .1. >. ] .~ e. ( Base ` L ) )
29 eqid 
 |-  ( +g ` R ) = ( +g ` R )
30 6 crngringd 
 |-  ( ph -> R e. Ring )
31 1 2 30 ringidcld 
 |-  ( ph -> .1. e. B )
32 eqid 
 |-  ( .r ` L ) = ( .r ` L )
33 1 24 29 4 3 6 7 31 15 8 18 32 rlocmulval 
 |-  ( ph -> ( [ <. .1. , Q >. ] .~ ( .r ` L ) [ <. Q , .1. >. ] .~ ) = [ <. ( .1. ( .r ` R ) Q ) , ( Q ( .r ` R ) .1. ) >. ] .~ )
34 1 23 2 24 25 26 3 6 7 erler 
 |-  ( ph -> .~ Er ( B X. S ) )
35 eqidd 
 |-  ( ph -> <. .1. , .1. >. = <. .1. , .1. >. )
36 1 24 2 30 15 ringlidmd 
 |-  ( ph -> ( .1. ( .r ` R ) Q ) = Q )
37 1 24 2 30 15 ringridmd 
 |-  ( ph -> ( Q ( .r ` R ) .1. ) = Q )
38 36 37 opeq12d 
 |-  ( ph -> <. ( .1. ( .r ` R ) Q ) , ( Q ( .r ` R ) .1. ) >. = <. Q , Q >. )
39 37 eqcomd 
 |-  ( ph -> Q = ( Q ( .r ` R ) .1. ) )
40 1 3 6 7 24 35 38 31 15 18 8 8 39 39 erlbr2d 
 |-  ( ph -> <. .1. , .1. >. .~ <. ( .1. ( .r ` R ) Q ) , ( Q ( .r ` R ) .1. ) >. )
41 34 40 erthi 
 |-  ( ph -> [ <. .1. , .1. >. ] .~ = [ <. ( .1. ( .r ` R ) Q ) , ( Q ( .r ` R ) .1. ) >. ] .~ )
42 eqid 
 |-  [ <. .1. , .1. >. ] .~ = [ <. .1. , .1. >. ] .~
43 23 2 4 3 6 7 42 rloc1r 
 |-  ( ph -> [ <. .1. , .1. >. ] .~ = ( 1r ` L ) )
44 33 41 43 3eqtr2d 
 |-  ( ph -> ( [ <. .1. , Q >. ] .~ ( .r ` L ) [ <. Q , .1. >. ] .~ ) = ( 1r ` L ) )
45 10 28 44 rspcedvdw 
 |-  ( ph -> E. a e. ( Base ` L ) ( [ <. .1. , Q >. ] .~ ( .r ` L ) a ) = ( 1r ` L ) )
46 eqid 
 |-  ( Base ` L ) = ( Base ` L )
47 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
48 31 8 opelxpd 
 |-  ( ph -> <. .1. , Q >. e. ( B X. S ) )
49 20 ecelqsi 
 |-  ( <. .1. , Q >. e. ( B X. S ) -> [ <. .1. , Q >. ] .~ e. ( ( B X. S ) /. .~ ) )
50 48 49 syl 
 |-  ( ph -> [ <. .1. , Q >. ] .~ e. ( ( B X. S ) /. .~ ) )
51 50 27 eleqtrd 
 |-  ( ph -> [ <. .1. , Q >. ] .~ e. ( Base ` L ) )
52 1 24 29 4 3 6 7 rloccring 
 |-  ( ph -> L e. CRing )
53 46 5 32 47 51 52 isunitc 
 |-  ( ph -> ( [ <. .1. , Q >. ] .~ e. W <-> E. a e. ( Base ` L ) ( [ <. .1. , Q >. ] .~ ( .r ` L ) a ) = ( 1r ` L ) ) )
54 45 53 mpbird 
 |-  ( ph -> [ <. .1. , Q >. ] .~ e. W )