This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 )
rloc0g.2 ⊢ 1 = ( 1r ‘ 𝑅 )
rloc0g.3 ⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
rloc0g.4 ⊢ ∼ = ( 𝑅 ~RL 𝑆 )
rloc0g.5 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rloc0g.6 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
rloc0g.o ⊢ 𝑂 = [ ⟨ 0 , 1 ⟩ ] ∼
Assertion rloc0g ( 𝜑 → 𝑂 = ( 0g ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 rloc0g.1 ⊢ 0 = ( 0g ‘ 𝑅 )
2 rloc0g.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 rloc0g.3 ⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
4 rloc0g.4 ⊢ ∼ = ( 𝑅 ~RL 𝑆 )
5 rloc0g.5 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 rloc0g.6 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
7 rloc0g.o ⊢ 𝑂 = [ ⟨ 0 , 1 ⟩ ] ∼
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11 8 9 10 3 4 5 6 rloccring ⊢ ( 𝜑 → 𝐿 ∈ CRing )
12 11 crnggrpd ⊢ ( 𝜑 → 𝐿 ∈ Grp )
13 5 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
14 8 1 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
15 13 14 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
16 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
17 16 2 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
18 17 subm0cl ⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 1 ∈ 𝑆 )
19 6 18 syl ⊢ ( 𝜑 → 1 ∈ 𝑆 )
20 15 19 opelxpd ⊢ ( 𝜑 → ⟨ 0 , 1 ⟩ ∈ ( ( Base ‘ 𝑅 ) × 𝑆 ) )
21 4 ovexi ⊢ ∼ ∈ V
22 21 ecelqsi ⊢ ( ⟨ 0 , 1 ⟩ ∈ ( ( Base ‘ 𝑅 ) × 𝑆 ) → [ ⟨ 0 , 1 ⟩ ] ∼ ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
23 20 22 syl ⊢ ( 𝜑 → [ ⟨ 0 , 1 ⟩ ] ∼ ∈ ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) )
24 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
25 eqid ⊢ ( ( Base ‘ 𝑅 ) × 𝑆 ) = ( ( Base ‘ 𝑅 ) × 𝑆 )
26 16 8 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
27 26 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
28 6 27 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
29 8 1 9 24 25 3 4 5 28 rlocbas ⊢ ( 𝜑 → ( ( ( Base ‘ 𝑅 ) × 𝑆 ) / ∼ ) = ( Base ‘ 𝐿 ) )
30 23 29 eleqtrd ⊢ ( 𝜑 → [ ⟨ 0 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) )
31 eqid ⊢ ( +g ‘ 𝐿 ) = ( +g ‘ 𝐿 )
32 8 9 10 3 4 5 6 15 15 19 19 31 rlocaddval ⊢ ( 𝜑 → ( [ ⟨ 0 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 0 , 1 ⟩ ] ∼ ) = [ ⟨ ( ( 0 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 0 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ )
33 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
34 8 9 2 33 15 ringridmd ⊢ ( 𝜑 → ( 0 ( .r ‘ 𝑅 ) 1 ) = 0 )
35 34 34 oveq12d ⊢ ( 𝜑 → ( ( 0 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 0 ( .r ‘ 𝑅 ) 1 ) ) = ( 0 ( +g ‘ 𝑅 ) 0 ) )
36 8 10 1 13 15 grplidd ⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) 0 ) = 0 )
37 35 36 eqtrd ⊢ ( 𝜑 → ( ( 0 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 0 ( .r ‘ 𝑅 ) 1 ) ) = 0 )
38 28 19 sseldd ⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
39 8 9 2 33 38 ringlidmd ⊢ ( 𝜑 → ( 1 ( .r ‘ 𝑅 ) 1 ) = 1 )
40 37 39 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 0 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 0 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ = ⟨ 0 , 1 ⟩ )
41 40 eceq1d ⊢ ( 𝜑 → [ ⟨ ( ( 0 ( .r ‘ 𝑅 ) 1 ) ( +g ‘ 𝑅 ) ( 0 ( .r ‘ 𝑅 ) 1 ) ) , ( 1 ( .r ‘ 𝑅 ) 1 ) ⟩ ] ∼ = [ ⟨ 0 , 1 ⟩ ] ∼ )
42 32 41 eqtrd ⊢ ( 𝜑 → ( [ ⟨ 0 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 0 , 1 ⟩ ] ∼ ) = [ ⟨ 0 , 1 ⟩ ] ∼ )
43 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
44 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
45 43 31 44 isgrpid2 ⊢ ( 𝐿 ∈ Grp → ( ( [ ⟨ 0 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ( [ ⟨ 0 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 0 , 1 ⟩ ] ∼ ) = [ ⟨ 0 , 1 ⟩ ] ∼ ) ↔ ( 0g ‘ 𝐿 ) = [ ⟨ 0 , 1 ⟩ ] ∼ ) )
46 45 biimpa ⊢ ( ( 𝐿 ∈ Grp ∧ ( [ ⟨ 0 , 1 ⟩ ] ∼ ∈ ( Base ‘ 𝐿 ) ∧ ( [ ⟨ 0 , 1 ⟩ ] ∼ ( +g ‘ 𝐿 ) [ ⟨ 0 , 1 ⟩ ] ∼ ) = [ ⟨ 0 , 1 ⟩ ] ∼ ) ) → ( 0g ‘ 𝐿 ) = [ ⟨ 0 , 1 ⟩ ] ∼ )
47 12 30 42 46 syl12anc ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = [ ⟨ 0 , 1 ⟩ ] ∼ )
48 7 47 eqtr4id ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ 𝐿 ) )