erld2

Description: Main property of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erld2.b	$⊢ B = {Base}_{R}$
	erld2.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	erld2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	erld2.r	$⊢ φ \to R \in CRing$
	erld2.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
	erld2.x	$⊢ φ \to X \in B$
	erld2.y	$⊢ φ \to Y \in S$
	erld2.z	$⊢ φ \to Z \in B$
	erld2.w	$⊢ φ \to W \in S$
	erld2.1	$⊢ φ \to [⟨X, Y⟩] \underset{˙}{\sim} = [⟨Z, W⟩] \underset{˙}{\sim}$
Assertion	erld2	$⊢ φ \to \exists t \in S t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		erld2.b	$⊢ B = {Base}_{R}$
2		erld2.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
3		erld2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		erld2.r	$⊢ φ \to R \in CRing$
5		erld2.s	$⊢ φ \to S \in SubMnd ({mulGrp}_{R})$
6		erld2.x	$⊢ φ \to X \in B$
7		erld2.y	$⊢ φ \to Y \in S$
8		erld2.z	$⊢ φ \to Z \in B$
9		erld2.w	$⊢ φ \to W \in S$
10		erld2.1	$⊢ φ \to [⟨X, Y⟩] \underset{˙}{\sim} = [⟨Z, W⟩] \underset{˙}{\sim}$
11		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
12	11 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
13	12	submss	$⊢ S \in SubMnd ({mulGrp}_{R}) \to S \subseteq B$
14	5 13	syl	$⊢ φ \to S \subseteq B$
15		eqid	$⊢ 0_{R} = 0_{R}$
16		eqid	$⊢ -_{R} = -_{R}$
17		eqid	$⊢ 1_{R} = 1_{R}$
18		eqid	$⊢ B \times S = B \times S$
19	1 15 17 3 16 18 2 4 5	erler	$⊢ φ \to \underset{˙}{\sim} Er (B \times S)$
20	6 7	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times S)$
21	19 20	erth	$⊢ φ \to (⟨X, Y⟩ \underset{˙}{\sim} ⟨Z, W⟩ \leftrightarrow [⟨X, Y⟩] \underset{˙}{\sim} = [⟨Z, W⟩] \underset{˙}{\sim})$
22	10 21	mpbird	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\sim} ⟨Z, W⟩$
23	1 2 14 15 3 16 22	erldi	$⊢ φ \to \exists t \in S t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}$
24	4	crngringd	$⊢ φ \to R \in Ring$
25	24	ringgrpd	$⊢ φ \to R \in Grp$
26	25	ad2antrr	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to R \in Grp$
27	24	adantr	$⊢ (φ \land t \in S) \to R \in Ring$
28	27	adantr	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to R \in Ring$
29	14	sselda	$⊢ (φ \land t \in S) \to t \in B$
30	29	adantr	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to t \in B$
31	14 9	sseldd	$⊢ φ \to W \in B$
32	1 3 24 6 31	ringcld	$⊢ φ \to X \underset{˙}{\cdot} W \in B$
33	32	adantr	$⊢ (φ \land t \in S) \to X \underset{˙}{\cdot} W \in B$
34	33	adantr	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to X \underset{˙}{\cdot} W \in B$
35	1 3 28 30 34	ringcld	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) \in B$
36	14 7	sseldd	$⊢ φ \to Y \in B$
37	1 3 24 8 36	ringcld	$⊢ φ \to Z \underset{˙}{\cdot} Y \in B$
38	37	adantr	$⊢ (φ \land t \in S) \to Z \underset{˙}{\cdot} Y \in B$
39	38	adantr	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to Z \underset{˙}{\cdot} Y \in B$
40	1 3 28 30 39	ringcld	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) \in B$
41		op1stg	$⊢ (X \in B \land Y \in S) \to 1^{st} (⟨X, Y⟩) = X$
42	6 7 41	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
43		op2ndg	$⊢ (Z \in B \land W \in S) \to 2^{nd} (⟨Z, W⟩) = W$
44	8 9 43	syl2anc	$⊢ φ \to 2^{nd} (⟨Z, W⟩) = W$
45	42 44	oveq12d	$⊢ φ \to 1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩) = X \underset{˙}{\cdot} W$
46		op1stg	$⊢ (Z \in B \land W \in S) \to 1^{st} (⟨Z, W⟩) = Z$
47	8 9 46	syl2anc	$⊢ φ \to 1^{st} (⟨Z, W⟩) = Z$
48		op2ndg	$⊢ (X \in B \land Y \in S) \to 2^{nd} (⟨X, Y⟩) = Y$
49	6 7 48	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
50	47 49	oveq12d	$⊢ φ \to 1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩) = Z \underset{˙}{\cdot} Y$
51	45 50	oveq12d	$⊢ φ \to (1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩)) = (X \underset{˙}{\cdot} W) -_{R} (Z \underset{˙}{\cdot} Y)$
52	51	oveq2d	$⊢ φ \to t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = t \underset{˙}{\cdot} ((X \underset{˙}{\cdot} W) -_{R} (Z \underset{˙}{\cdot} Y))$
53	52	adantr	$⊢ (φ \land t \in S) \to t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = t \underset{˙}{\cdot} ((X \underset{˙}{\cdot} W) -_{R} (Z \underset{˙}{\cdot} Y))$
54	1 3 16 27 29 33 38	ringsubdi	$⊢ (φ \land t \in S) \to t \underset{˙}{\cdot} ((X \underset{˙}{\cdot} W) -_{R} (Z \underset{˙}{\cdot} Y)) = (t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y))$
55	53 54	eqtrd	$⊢ (φ \land t \in S) \to t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = (t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y))$
56	55	eqeq1d	$⊢ (φ \land t \in S) \to (t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R} \leftrightarrow (t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) = 0_{R})$
57	56	biimpa	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to (t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) = 0_{R}$
58	1 15 16	grpsubeq0	$⊢ (R \in Grp \land t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) \in B \land t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) \in B) \to ((t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) = 0_{R} \leftrightarrow t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y))$
59	58	biimpa	$⊢ ((R \in Grp \land t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) \in B \land t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y) \in B) \land (t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W)) -_{R} (t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)) = 0_{R}) \to t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
60	26 35 40 57 59	syl31anc	$⊢ ((φ \land t \in S) \land t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R}) \to t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
61	60	ex	$⊢ (φ \land t \in S) \to (t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R} \to t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y))$
62	61	reximdva	$⊢ φ \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (⟨X, Y⟩) \underset{˙}{\cdot} 2^{nd} (⟨Z, W⟩)) -_{R} (1^{st} (⟨Z, W⟩) \underset{˙}{\cdot} 2^{nd} (⟨X, Y⟩))) = 0_{R} \to \exists t \in S t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y))$
63	23 62	mpd	$⊢ φ \to \exists t \in S t \underset{˙}{\cdot} (X \underset{˙}{\cdot} W) = t \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem erld2

Proof