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 = {Base}_{R}$
	erlbr2d.q	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	erlbr2d.r	$⊢ φ \to R \in CRing$
	erlbr2d.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
	erlbr2d.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	erlbr2d.u	$⊢ φ \to U = ⟨E, G⟩$
	erlbr2d.v	$⊢ φ \to V = ⟨F, H⟩$
	erlbr2d.e	$⊢ φ \to E \in B$
	erlbr2d.f	$⊢ φ \to F \in B$
	erlbr2d.g	$⊢ φ \to G \in S$
	erlbr2d.h	$⊢ φ \to H \in S$
	erlbr2d.1	$⊢ φ \to T \in S$
	erlbr2d.2	$⊢ φ \to F = T \underset{˙}{\cdot} E$
	erlbr2d.3	$⊢ φ \to H = T \underset{˙}{\cdot} G$
Assertion	erlbr2d	$⊢ φ \to U \underset{˙}{\sim} V$

Proof

Step	Hyp	Ref	Expression
1		erlbr2d.b	$⊢ B = {Base}_{R}$
2		erlbr2d.q	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
3		erlbr2d.r	$⊢ φ \to R \in CRing$
4		erlbr2d.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
5		erlbr2d.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		erlbr2d.u	$⊢ φ \to U = ⟨E, G⟩$
7		erlbr2d.v	$⊢ φ \to V = ⟨F, H⟩$
8		erlbr2d.e	$⊢ φ \to E \in B$
9		erlbr2d.f	$⊢ φ \to F \in B$
10		erlbr2d.g	$⊢ φ \to G \in S$
11		erlbr2d.h	$⊢ φ \to H \in S$
12		erlbr2d.1	$⊢ φ \to T \in S$
13		erlbr2d.2	$⊢ φ \to F = T \underset{˙}{\cdot} E$
14		erlbr2d.3	$⊢ φ \to H = T \underset{˙}{\cdot} G$
15		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
16	15 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
17	16	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
18	4 17	syl	$⊢ φ \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_{{mulGrp}_{R}}$
23	22	subm0cl	$⊢ S \in SubMnd ({mulGrp}_{R}) \to 1_{R} \in S$
24	4 23	syl	$⊢ φ \to 1_{R} \in S$
25	14	oveq2d	$⊢ φ \to E \underset{˙}{\cdot} H = E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)$
26	13	oveq1d	$⊢ φ \to F \underset{˙}{\cdot} G = (T \underset{˙}{\cdot} E) \underset{˙}{\cdot} G$
27	25 26	oveq12d	$⊢ φ \to (E \underset{˙}{\cdot} H) -_{R} (F \underset{˙}{\cdot} G) = (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) -_{R} ((T \underset{˙}{\cdot} E) \underset{˙}{\cdot} G)$
28	18 12	sseldd	$⊢ φ \to T \in B$
29	18 10	sseldd	$⊢ φ \to G \in B$
30	1 5 3 28 8 29	crng32d	$⊢ φ \to (T \underset{˙}{\cdot} E) \underset{˙}{\cdot} G = (T \underset{˙}{\cdot} G) \underset{˙}{\cdot} E$
31	3	crngringd	$⊢ φ \to R \in Ring$
32	1 5 31 28 29	ringcld	$⊢ φ \to T \underset{˙}{\cdot} G \in B$
33	1 5 3 32 8	crngcomd	$⊢ φ \to (T \underset{˙}{\cdot} G) \underset{˙}{\cdot} E = E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)$
34	30 33	eqtrd	$⊢ φ \to (T \underset{˙}{\cdot} E) \underset{˙}{\cdot} G = E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)$
35	34	oveq2d	$⊢ φ \to (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) -_{R} ((T \underset{˙}{\cdot} E) \underset{˙}{\cdot} G) = (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) -_{R} (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G))$
36	3	crnggrpd	$⊢ φ \to R \in Grp$
37	1 5 31 8 32	ringcld	$⊢ φ \to E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G) \in B$
38	1 19 20	grpsubid	$⊢ (R \in Grp \land E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G) \in B) \to (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) -_{R} (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) = 0_{R}$
39	36 37 38	syl2anc	$⊢ φ \to (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) -_{R} (E \underset{˙}{\cdot} (T \underset{˙}{\cdot} G)) = 0_{R}$
40	27 35 39	3eqtrd	$⊢ φ \to (E \underset{˙}{\cdot} H) -_{R} (F \underset{˙}{\cdot} G) = 0_{R}$
41	40	oveq2d	$⊢ φ \to 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (F \underset{˙}{\cdot} G)) = 1_{R} \underset{˙}{\cdot} 0_{R}$
42	18 24	sseldd	$⊢ φ \to 1_{R} \in B$
43	1 5 19 31 42	ringrzd	$⊢ φ \to 1_{R} \underset{˙}{\cdot} 0_{R} = 0_{R}$
44	41 43	eqtrd	$⊢ φ \to 1_{R} \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) -_{R} (F \underset{˙}{\cdot} G)) = 0_{R}$
45	1 2 18 19 5 20 6 7 8 9 10 11 24 44	erlbrd	$⊢ φ \to U \underset{˙}{\sim} V$

Metamath Proof Explorer

Theorem erlbr2d

Proof