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 ‘ 𝐿 ) )