erlcl1

Description: Closure for the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erlcl1.b	$⊢ B = {Base}_{R}$
	erlcl1.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
	erlcl1.s	$⊢ φ \to S \subseteq B$
	erlcl1.1	$⊢ φ \to U \underset{˙}{\sim} V$
Assertion	erlcl1	$⊢ φ \to U \in (B \times S)$

Proof

Step	Hyp	Ref	Expression
1		erlcl1.b	$⊢ B = {Base}_{R}$
2		erlcl1.e	$⊢ \underset{˙}{\sim} = R ~_{RL} S$
3		erlcl1.s	$⊢ φ \to S \subseteq B$
4		erlcl1.1	$⊢ φ \to U \underset{˙}{\sim} V$
5		eqid	$⊢ 0_{R} = 0_{R}$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		eqid	$⊢ -_{R} = -_{R}$
8		eqid	$⊢ B \times S = B \times S$
9		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R})\} = \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R})\}$
10	1 5 6 7 8 9 3	erlval	$⊢ φ \to R ~_{RL} S = \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R})\}$
11	2 10	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R})\}$
12		simpl	$⊢ (a = U \land b = V) \to a = U$
13	12	fveq2d	$⊢ (a = U \land b = V) \to 1^{st} (a) = 1^{st} (U)$
14		simpr	$⊢ (a = U \land b = V) \to b = V$
15	14	fveq2d	$⊢ (a = U \land b = V) \to 2^{nd} (b) = 2^{nd} (V)$
16	13 15	oveq12d	$⊢ (a = U \land b = V) \to 1^{st} (a) \cdot_{R} 2^{nd} (b) = 1^{st} (U) \cdot_{R} 2^{nd} (V)$
17	14	fveq2d	$⊢ (a = U \land b = V) \to 1^{st} (b) = 1^{st} (V)$
18	12	fveq2d	$⊢ (a = U \land b = V) \to 2^{nd} (a) = 2^{nd} (U)$
19	17 18	oveq12d	$⊢ (a = U \land b = V) \to 1^{st} (b) \cdot_{R} 2^{nd} (a) = 1^{st} (V) \cdot_{R} 2^{nd} (U)$
20	16 19	oveq12d	$⊢ (a = U \land b = V) \to (1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a)) = (1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))$
21	20	oveq2d	$⊢ (a = U \land b = V) \to t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U)))$
22	21	eqeq1d	$⊢ (a = U \land b = V) \to (t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R} \leftrightarrow t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))) = 0_{R})$
23	22	rexbidv	$⊢ (a = U \land b = V) \to (\exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R} \leftrightarrow \exists t \in S t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))) = 0_{R})$
24	23	adantl	$⊢ (φ \land (a = U \land b = V)) \to (\exists t \in S t \cdot_{R} ((1^{st} (a) \cdot_{R} 2^{nd} (b)) -_{R} (1^{st} (b) \cdot_{R} 2^{nd} (a))) = 0_{R} \leftrightarrow \exists t \in S t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))) = 0_{R})$
25	11 24	brab2d	$⊢ φ \to (U \underset{˙}{\sim} V \leftrightarrow ((U \in (B \times S) \land V \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))) = 0_{R}))$
26	4 25	mpbid	$⊢ φ \to ((U \in (B \times S) \land V \in (B \times S)) \land \exists t \in S t \cdot_{R} ((1^{st} (U) \cdot_{R} 2^{nd} (V)) -_{R} (1^{st} (V) \cdot_{R} 2^{nd} (U))) = 0_{R})$
27	26	simplld	$⊢ φ \to U \in (B \times S)$

Metamath Proof Explorer

Theorem erlcl1

Proof