Metamath Proof Explorer

Theorem rloc0g

Description: The zero 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 ) ) )
rloc0g.o 
|- O = [ <. .0. , .1. >. ] .~
Assertion rloc0g 
|- ( ph -> O = ( 0g ` 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 rloc0g.o 
 |-  O = [ <. .0. , .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 crnggrpd 
 |-  ( ph -> L e. Grp )
13 5 crnggrpd 
 |-  ( ph -> R e. Grp )
14 8 1 grpidcl 
 |-  ( R e. Grp -> .0. e. ( Base ` R ) )
15 13 14 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
16 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
17 16 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 15 19 opelxpd 
 |-  ( ph -> <. .0. , .1. >. e. ( ( Base ` R ) X. S ) )
21 4 ovexi 
 |-  .~ e. _V
22 21 ecelqsi 
 |-  ( <. .0. , .1. >. e. ( ( Base ` R ) X. S ) -> [ <. .0. , .1. >. ] .~ e. ( ( ( Base ` R ) X. S ) /. .~ ) )
23 20 22 syl 
 |-  ( ph -> [ <. .0. , .1. >. ] .~ e. ( ( ( Base ` R ) X. S ) /. .~ ) )
24 eqid 
 |-  ( -g ` R ) = ( -g ` R )
25 eqid 
 |-  ( ( Base ` R ) X. S ) = ( ( Base ` R ) X. S )
26 16 8 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
27 26 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ ( Base ` R ) )
28 6 27 syl 
 |-  ( ph -> S C_ ( Base ` R ) )
29 8 1 9 24 25 3 4 5 28 rlocbas 
 |-  ( ph -> ( ( ( Base ` R ) X. S ) /. .~ ) = ( Base ` L ) )
30 23 29 eleqtrd 
 |-  ( ph -> [ <. .0. , .1. >. ] .~ e. ( Base ` L ) )
31 eqid 
 |-  ( +g ` L ) = ( +g ` L )
32 8 9 10 3 4 5 6 15 15 19 19 31 rlocaddval 
 |-  ( ph -> ( [ <. .0. , .1. >. ] .~ ( +g ` L ) [ <. .0. , .1. >. ] .~ ) = [ <. ( ( .0. ( .r ` R ) .1. ) ( +g ` R ) ( .0. ( .r ` R ) .1. ) ) , ( .1. ( .r ` R ) .1. ) >. ] .~ )
33 5 crngringd 
 |-  ( ph -> R e. Ring )
34 8 9 2 33 15 ringridmd 
 |-  ( ph -> ( .0. ( .r ` R ) .1. ) = .0. )
35 34 34 oveq12d 
 |-  ( ph -> ( ( .0. ( .r ` R ) .1. ) ( +g ` R ) ( .0. ( .r ` R ) .1. ) ) = ( .0. ( +g ` R ) .0. ) )
36 8 10 1 13 15 grplidd 
 |-  ( ph -> ( .0. ( +g ` R ) .0. ) = .0. )
37 35 36 eqtrd 
 |-  ( ph -> ( ( .0. ( .r ` R ) .1. ) ( +g ` R ) ( .0. ( .r ` R ) .1. ) ) = .0. )
38 28 19 sseldd 
 |-  ( ph -> .1. e. ( Base ` R ) )
39 8 9 2 33 38 ringlidmd 
 |-  ( ph -> ( .1. ( .r ` R ) .1. ) = .1. )
40 37 39 opeq12d 
 |-  ( ph -> <. ( ( .0. ( .r ` R ) .1. ) ( +g ` R ) ( .0. ( .r ` R ) .1. ) ) , ( .1. ( .r ` R ) .1. ) >. = <. .0. , .1. >. )
41 40 eceq1d 
 |-  ( ph -> [ <. ( ( .0. ( .r ` R ) .1. ) ( +g ` R ) ( .0. ( .r ` R ) .1. ) ) , ( .1. ( .r ` R ) .1. ) >. ] .~ = [ <. .0. , .1. >. ] .~ )
42 32 41 eqtrd 
 |-  ( ph -> ( [ <. .0. , .1. >. ] .~ ( +g ` L ) [ <. .0. , .1. >. ] .~ ) = [ <. .0. , .1. >. ] .~ )
43 eqid 
 |-  ( Base ` L ) = ( Base ` L )
44 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
45 43 31 44 isgrpid2 
 |-  ( L e. Grp -> ( ( [ <. .0. , .1. >. ] .~ e. ( Base ` L ) /\ ( [ <. .0. , .1. >. ] .~ ( +g ` L ) [ <. .0. , .1. >. ] .~ ) = [ <. .0. , .1. >. ] .~ ) <-> ( 0g ` L ) = [ <. .0. , .1. >. ] .~ ) )
46 45 biimpa 
 |-  ( ( L e. Grp /\ ( [ <. .0. , .1. >. ] .~ e. ( Base ` L ) /\ ( [ <. .0. , .1. >. ] .~ ( +g ` L ) [ <. .0. , .1. >. ] .~ ) = [ <. .0. , .1. >. ] .~ ) ) -> ( 0g ` L ) = [ <. .0. , .1. >. ] .~ )
47 12 30 42 46 syl12anc 
 |-  ( ph -> ( 0g ` L ) = [ <. .0. , .1. >. ] .~ )
48 7 47 eqtr4id 
 |-  ( ph -> O = ( 0g ` L ) )