Theorem rloc0g

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

	Ref	Expression
Hypotheses	rloc0g.1	$$⊢\underset{\dot{}}{0}=0_R$$
	rloc0g.2	$$⊢\underset{\dot{}}{1}=1_R$$
	rloc0g.3	No typesetting found for |- L = ( R RLocal S ) with typecode |-
	rloc0g.4	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	rloc0g.5	$$⊢\phi \to R\in \mathrm{CRing}$$
	rloc0g.6	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
	rloc0g.o	$$⊢O=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
Assertion	rloc0g	$$⊢\phi \to O=0_L$$

Proof

Step	Hyp	Ref	Expression
1		rloc0g.1	$$⊢\underset{\dot{}}{0}=0_R$$
2		rloc0g.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		rloc0g.3	Could not format L = ( R RLocal S ) : No typesetting found for |- L = ( R RLocal S ) with typecode |-
4		rloc0g.4	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
5		rloc0g.5	$$⊢\phi \to R\in \mathrm{CRing}$$
6		rloc0g.6	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
7		rloc0g.o	$$⊢O=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9		eqid	$$⊢{\cdot }_R={\cdot }_R$$
10		eqid	$$⊢{+}_R={+}_R$$
11	8 9 10 3 4 5 6	rloccring	$$⊢\phi \to L\in \mathrm{CRing}$$
12	11	crnggrpd	$$⊢\phi \to L\in \mathrm{Grp}$$
13	5	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
14	8 1	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
15	13 14	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
16		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
17	16 2	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
18	17	subm0cl	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to \underset{\dot{}}{1}\in S$$
19	6 18	syl	$$⊢\phi \to \underset{\dot{}}{1}\in S$$
20	15 19	opelxpd	$$⊢\phi \to ⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\in \left({\mathrm{Base}}_R\times S\right)$$
21	4	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
22	21	ecelqsi	$$⊢⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\in \left({\mathrm{Base}}_R\times S\right)\to \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in \left(\left({\mathrm{Base}}_R\times S\right)/\underset{\dot{}}{\sim }\right)$$
23	20 22	syl	$$⊢\phi \to \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in \left(\left({\mathrm{Base}}_R\times S\right)/\underset{\dot{}}{\sim }\right)$$
24		eqid	$$⊢{-}_R={-}_R$$
25		eqid	$$⊢{\mathrm{Base}}_R\times S={\mathrm{Base}}_R\times S$$
26	16 8	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
27	26	submss	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to S\subseteq {\mathrm{Base}}_R$$
28	6 27	syl	$$⊢\phi \to S\subseteq {\mathrm{Base}}_R$$
29	8 1 9 24 25 3 4 5 28	rlocbas	$$⊢\phi \to \left({\mathrm{Base}}_R\times S\right)/\underset{\dot{}}{\sim }={\mathrm{Base}}_L$$
30	23 29	eleqtrd	$$⊢\phi \to \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_L$$
31		eqid	$$⊢{+}_L={+}_L$$
32	8 9 10 3 4 5 6 15 15 19 19 31	rlocaddval	$$⊢\phi \to \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }{+}_L\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right){+}_R\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right),\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
33	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
34	8 9 2 33 15	ringridmd	$$⊢\phi \to \underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
35	34 34	oveq12d	$$⊢\phi \to \left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right){+}_R\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}$$
36	8 10 1 13 15	grplidd	$$⊢\phi \to \underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
37	35 36	eqtrd	$$⊢\phi \to \left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right){+}_R\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right)=\underset{\dot{}}{0}$$
38	28 19	sseldd	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
39	8 9 2 33 38	ringlidmd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
40	37 39	opeq12d	$$⊢\phi \to ⟨\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right){+}_R\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right),\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}⟩=⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩$$
41	40	eceq1d	$$⊢\phi \to \left[⟨\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right){+}_R\left(\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{1}\right),\underset{\dot{}}{1}{\cdot }_R\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
42	32 41	eqtrd	$$⊢\phi \to \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }{+}_L\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
43		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
44		eqid	$$⊢0_L=0_L$$
45	43 31 44	isgrpid2	$$⊢L\in \mathrm{Grp}\to \left(\left(\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_L\wedge \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }{+}_L\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)\leftrightarrow 0_L=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)$$
46	45	biimpa	$$⊢\left(L\in \mathrm{Grp}\wedge \left(\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_L\wedge \left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }{+}_L\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }\right)\right)\to 0_L=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
47	12 30 42 46	syl12anc	$$⊢\phi \to 0_L=\left[⟨\underset{\dot{}}{0},\underset{\dot{}}{1}⟩\right]\underset{\dot{}}{\sim }$$
48	7 47	eqtr4id	$$⊢\phi \to O=0_L$$