Metamath Proof Explorer

Theorem rloc1r

Description: The multiplicative identity of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses rloc0g.1 
|- .0. = ( 0g ` R )
rloc0g.2 
|- .1. = ( 1r ` R )
rloc0g.3 
|- L = ( R RLocal S )
rloc0g.4 
|- .~ = ( R ~RL S )
rloc0g.5 
|- ( ph -> R e. CRing )
rloc0g.6 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
rloc1r.i 
|- I = [ <. .1. , .1. >. ] .~
Assertion rloc1r 
|- ( ph -> I = ( 1r ` L ) )

Proof

Step Hyp Ref Expression
1 rloc0g.1 
 |-  .0. = ( 0g ` R )
2 rloc0g.2 
 |-  .1. = ( 1r ` R )
3 rloc0g.3 
 |-  L = ( R RLocal S )
4 rloc0g.4 
 |-  .~ = ( R ~RL S )
5 rloc0g.5 
 |-  ( ph -> R e. CRing )
6 rloc0g.6 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
7 rloc1r.i 
 |-  I = [ <. .1. , .1. >. ] .~
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 8 9 10 3 4 5 6 rloccring 
 |-  ( ph -> L e. CRing )
12 11 crngringd 
 |-  ( ph -> L e. Ring )
13 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
14 13 8 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
15 14 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ ( Base ` R ) )
16 6 15 syl 
 |-  ( ph -> S C_ ( Base ` R ) )
17 13 2 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
18 17 subm0cl 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> .1. e. S )
19 6 18 syl 
 |-  ( ph -> .1. e. S )
20 16 19 sseldd 
 |-  ( ph -> .1. e. ( Base ` R ) )
21 20 19 opelxpd 
 |-  ( ph -> <. .1. , .1. >. e. ( ( Base ` R ) X. S ) )
22 4 ovexi 
 |-  .~ e. _V
23 22 ecelqsi 
 |-  ( <. .1. , .1. >. e. ( ( Base ` R ) X. S ) -> [ <. .1. , .1. >. ] .~ e. ( ( ( Base ` R ) X. S ) /. .~ ) )
24 21 23 syl 
 |-  ( ph -> [ <. .1. , .1. >. ] .~ e. ( ( ( Base ` R ) X. S ) /. .~ ) )
25 eqid 
 |-  ( -g ` R ) = ( -g ` R )
26 eqid 
 |-  ( ( Base ` R ) X. S ) = ( ( Base ` R ) X. S )
27 8 1 9 25 26 3 4 5 16 rlocbas 
 |-  ( ph -> ( ( ( Base ` R ) X. S ) /. .~ ) = ( Base ` L ) )
28 24 27 eleqtrd 
 |-  ( ph -> [ <. .1. , .1. >. ] .~ e. ( Base ` L ) )
29 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> R e. CRing )
30 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
31 20 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> .1. e. ( Base ` R ) )
32 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> a e. ( Base ` R ) )
33 30 18 syl 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> .1. e. S )
34 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> b e. S )
35 eqid 
 |-  ( .r ` L ) = ( .r ` L )
36 8 9 10 3 4 29 30 31 32 33 34 35 rlocmulval 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. .1. , .1. >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) = [ <. ( .1. ( .r ` R ) a ) , ( .1. ( .r ` R ) b ) >. ] .~ )
37 29 crngringd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> R e. Ring )
38 8 9 2 37 32 ringlidmd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( .1. ( .r ` R ) a ) = a )
39 30 15 syl 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> S C_ ( Base ` R ) )
40 39 34 sseldd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> b e. ( Base ` R ) )
41 8 9 2 37 40 ringlidmd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( .1. ( .r ` R ) b ) = b )
42 38 41 opeq12d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( .1. ( .r ` R ) a ) , ( .1. ( .r ` R ) b ) >. = <. a , b >. )
43 42 eceq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( .1. ( .r ` R ) a ) , ( .1. ( .r ` R ) b ) >. ] .~ = [ <. a , b >. ] .~ )
44 36 43 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. .1. , .1. >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) = [ <. a , b >. ] .~ )
45 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> x = [ <. a , b >. ] .~ )
46 45 oveq2d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = ( [ <. .1. , .1. >. ] .~ ( .r ` L ) [ <. a , b >. ] .~ ) )
47 44 46 45 3eqtr4d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x )
48 27 eqcomd 
 |-  ( ph -> ( Base ` L ) = ( ( ( Base ` R ) X. S ) /. .~ ) )
49 48 eleq2d 
 |-  ( ph -> ( x e. ( Base ` L ) <-> x e. ( ( ( Base ` R ) X. S ) /. .~ ) ) )
50 49 biimpa 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> x e. ( ( ( Base ` R ) X. S ) /. .~ ) )
51 50 elrlocbasi 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> E. a e. ( Base ` R ) E. b e. S x = [ <. a , b >. ] .~ )
52 47 51 r19.29vva 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x )
53 8 9 10 3 4 29 30 32 31 34 33 35 rlocmulval 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = [ <. ( a ( .r ` R ) .1. ) , ( b ( .r ` R ) .1. ) >. ] .~ )
54 8 9 2 37 32 ringridmd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( a ( .r ` R ) .1. ) = a )
55 8 9 2 37 40 ringridmd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( b ( .r ` R ) .1. ) = b )
56 54 55 opeq12d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> <. ( a ( .r ` R ) .1. ) , ( b ( .r ` R ) .1. ) >. = <. a , b >. )
57 56 eceq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> [ <. ( a ( .r ` R ) .1. ) , ( b ( .r ` R ) .1. ) >. ] .~ = [ <. a , b >. ] .~ )
58 53 57 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( [ <. a , b >. ] .~ ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = [ <. a , b >. ] .~ )
59 45 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = ( [ <. a , b >. ] .~ ( .r ` L ) [ <. .1. , .1. >. ] .~ ) )
60 58 59 45 3eqtr4d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ a e. ( Base ` R ) ) /\ b e. S ) /\ x = [ <. a , b >. ] .~ ) -> ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x )
61 60 51 r19.29vva 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x )
62 52 61 jca 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> ( ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x /\ ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x ) )
63 62 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` L ) ( ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x /\ ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x ) )
64 eqid 
 |-  ( Base ` L ) = ( Base ` L )
65 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
66 64 35 65 isringid 
 |-  ( L e. Ring -> ( ( [ <. .1. , .1. >. ] .~ e. ( Base ` L ) /\ A. x e. ( Base ` L ) ( ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x /\ ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x ) ) <-> ( 1r ` L ) = [ <. .1. , .1. >. ] .~ ) )
67 66 biimpa 
 |-  ( ( L e. Ring /\ ( [ <. .1. , .1. >. ] .~ e. ( Base ` L ) /\ A. x e. ( Base ` L ) ( ( [ <. .1. , .1. >. ] .~ ( .r ` L ) x ) = x /\ ( x ( .r ` L ) [ <. .1. , .1. >. ] .~ ) = x ) ) ) -> ( 1r ` L ) = [ <. .1. , .1. >. ] .~ )
68 12 28 63 67 syl12anc 
 |-  ( ph -> ( 1r ` L ) = [ <. .1. , .1. >. ] .~ )
69 7 68 eqtr4id 
 |-  ( ph -> I = ( 1r ` L ) )