Theorem erlbr2d

Description: Deduce the ring localization equivalence relation. Pairs <. E , G >. and <. T x. E , T x. G >. for T e. S are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erlbr2d.b	$$⊢B={\mathrm{Base}}_R$$
	erlbr2d.q	No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
	erlbr2d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	erlbr2d.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
	erlbr2d.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	erlbr2d.u	$$⊢\phi \to U=⟨E,G⟩$$
	erlbr2d.v	$$⊢\phi \to V=⟨F,H⟩$$
	erlbr2d.e	$$⊢\phi \to E\in B$$
	erlbr2d.f	$$⊢\phi \to F\in B$$
	erlbr2d.g	$$⊢\phi \to G\in S$$
	erlbr2d.h	$$⊢\phi \to H\in S$$
	erlbr2d.1	$$⊢\phi \to T\in S$$
	erlbr2d.2	$$⊢\phi \to F=T\underset{\dot{}}{·}E$$
	erlbr2d.3	$$⊢\phi \to H=T\underset{\dot{}}{·}G$$
Assertion	erlbr2d	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$

Proof

Step	Hyp	Ref	Expression
1		erlbr2d.b	$$⊢B={\mathrm{Base}}_R$$
2		erlbr2d.q	Could not format .~ = ( R ~RL S ) : No typesetting found for |- .~ = ( R ~RL S ) with typecode |-
3		erlbr2d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		erlbr2d.s	$$⊢\phi \to S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)$$
5		erlbr2d.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		erlbr2d.u	$$⊢\phi \to U=⟨E,G⟩$$
7		erlbr2d.v	$$⊢\phi \to V=⟨F,H⟩$$
8		erlbr2d.e	$$⊢\phi \to E\in B$$
9		erlbr2d.f	$$⊢\phi \to F\in B$$
10		erlbr2d.g	$$⊢\phi \to G\in S$$
11		erlbr2d.h	$$⊢\phi \to H\in S$$
12		erlbr2d.1	$$⊢\phi \to T\in S$$
13		erlbr2d.2	$$⊢\phi \to F=T\underset{\dot{}}{·}E$$
14		erlbr2d.3	$$⊢\phi \to H=T\underset{\dot{}}{·}G$$
15		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
16	15 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
17	16	submss	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to S\subseteq B$$
18	4 17	syl	$$⊢\phi \to S\subseteq B$$
19		eqid	$$⊢0_R=0_R$$
20		eqid	$$⊢{-}_R={-}_R$$
21		eqid	$$⊢1_R=1_R$$
22	15 21	ringidval	$$⊢1_R=0_{{\mathrm{mulGrp}}_R}$$
23	22	subm0cl	$$⊢S\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_R\right)\to 1_R\in S$$
24	4 23	syl	$$⊢\phi \to 1_R\in S$$
25	14	oveq2d	$$⊢\phi \to E\underset{\dot{}}{·}H=E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)$$
26	13	oveq1d	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(T\underset{\dot{}}{·}E\right)\underset{\dot{}}{·}G$$
27	25 26	oveq12d	$$⊢\phi \to \left(E\underset{\dot{}}{·}H\right){-}_R\left(F\underset{\dot{}}{·}G\right)=\left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right){-}_R\left(\left(T\underset{\dot{}}{·}E\right)\underset{\dot{}}{·}G\right)$$
28	18 12	sseldd	$$⊢\phi \to T\in B$$
29	18 10	sseldd	$$⊢\phi \to G\in B$$
30	1 5 3 28 8 29	cringmul32d	$$⊢\phi \to \left(T\underset{\dot{}}{·}E\right)\underset{\dot{}}{·}G=\left(T\underset{\dot{}}{·}G\right)\underset{\dot{}}{·}E$$
31	3	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
32	1 5 31 28 29	ringcld	$$⊢\phi \to T\underset{\dot{}}{·}G\in B$$
33	1 5 3 32 8	crngcomd	$$⊢\phi \to \left(T\underset{\dot{}}{·}G\right)\underset{\dot{}}{·}E=E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)$$
34	30 33	eqtrd	$$⊢\phi \to \left(T\underset{\dot{}}{·}E\right)\underset{\dot{}}{·}G=E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)$$
35	34	oveq2d	$$⊢\phi \to \left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right){-}_R\left(\left(T\underset{\dot{}}{·}E\right)\underset{\dot{}}{·}G\right)=\left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right){-}_R\left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right)$$
36	3	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
37	1 5 31 8 32	ringcld	$$⊢\phi \to E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\in B$$
38	1 19 20	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\in B\right)\to \left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right){-}_R\left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right)=0_R$$
39	36 37 38	syl2anc	$$⊢\phi \to \left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right){-}_R\left(E\underset{\dot{}}{·}\left(T\underset{\dot{}}{·}G\right)\right)=0_R$$
40	27 35 39	3eqtrd	$$⊢\phi \to \left(E\underset{\dot{}}{·}H\right){-}_R\left(F\underset{\dot{}}{·}G\right)=0_R$$
41	40	oveq2d	$$⊢\phi \to 1_R\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{·}H\right){-}_R\left(F\underset{\dot{}}{·}G\right)\right)=1_R\underset{\dot{}}{·}{0}_R$$
42	18 24	sseldd	$$⊢\phi \to 1_R\in B$$
43	1 5 19 31 42	ringrzd	$$⊢\phi \to 1_R\underset{\dot{}}{·}{0}_R=0_R$$
44	41 43	eqtrd	$$⊢\phi \to 1_R\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{·}H\right){-}_R\left(F\underset{\dot{}}{·}G\right)\right)=0_R$$
45	1 2 18 19 5 20 6 7 8 9 10 11 24 44	erlbrd	$$⊢\phi \to U\underset{\dot{}}{\sim }V$$