erlbrd

Description: Deduce the ring localization equivalence relation. If for some T e. S we have T x. ( E x. H - F x. G ) = 0 , then pairs <. E , G >. and <. F , H >. are equivalent under the localization relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	erlcl1.b	$⊢ B = {Base}_{R}$
	erlcl1.e	No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
	erlcl1.s	$⊢ φ \to S \subseteq B$
	erldi.1	$⊢ \underset{˙}{0} = 0_{R}$
	erldi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	erldi.3	$⊢ \underset{˙}{-} = -_{R}$
	erlbrd.u	$⊢ φ \to U = ⟨E, G⟩$
	erlbrd.v	$⊢ φ \to V = ⟨F, H⟩$
	erlbrd.e	$⊢ φ \to E \in B$
	erlbrd.f	$⊢ φ \to F \in B$
	erlbrd.g	$⊢ φ \to G \in S$
	erlbrd.h	$⊢ φ \to H \in S$
	erlbrd.1	$⊢ φ \to T \in S$
	erlbrd.2	$⊢ φ \to T \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0}$
Assertion	erlbrd	$⊢ φ \to U \underset{˙}{\sim} V$

Proof

Step	Hyp	Ref	Expression
1		erlcl1.b	$⊢ B = {Base}_{R}$
2		erlcl1.e	Could not format .~ = ( R ~RL S ) : No typesetting found for \|- .~ = ( R ~RL S ) with typecode \|-
3		erlcl1.s	$⊢ φ \to S \subseteq B$
4		erldi.1	$⊢ \underset{˙}{0} = 0_{R}$
5		erldi.2	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		erldi.3	$⊢ \underset{˙}{-} = -_{R}$
7		erlbrd.u	$⊢ φ \to U = ⟨E, G⟩$
8		erlbrd.v	$⊢ φ \to V = ⟨F, H⟩$
9		erlbrd.e	$⊢ φ \to E \in B$
10		erlbrd.f	$⊢ φ \to F \in B$
11		erlbrd.g	$⊢ φ \to G \in S$
12		erlbrd.h	$⊢ φ \to H \in S$
13		erlbrd.1	$⊢ φ \to T \in S$
14		erlbrd.2	$⊢ φ \to T \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0}$
15	9 11	opelxpd	$⊢ φ \to ⟨E, G⟩ \in (B \times S)$
16	7 15	eqeltrd	$⊢ φ \to U \in (B \times S)$
17	10 12	opelxpd	$⊢ φ \to ⟨F, H⟩ \in (B \times S)$
18	8 17	eqeltrd	$⊢ φ \to V \in (B \times S)$
19	16 18	jca	$⊢ φ \to (U \in (B \times S) \land V \in (B \times S))$
20		simpr	$⊢ (φ \land t = T) \to t = T$
21	20	oveq1d	$⊢ (φ \land t = T) \to t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = T \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G))$
22	21	eqeq1d	$⊢ (φ \land t = T) \to (t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0} \leftrightarrow T \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0})$
23	13 22 14	rspcedvd	$⊢ φ \to \exists t \in S t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0}$
24	19 23	jca	$⊢ φ \to ((U \in (B \times S) \land V \in (B \times S)) \land \exists t \in S t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0})$
25		eqid	$⊢ B \times S = B \times S$
26		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\} = \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
27	1 4 5 6 25 26 3	erlval	Could not format ( ph -> ( R ~RL S ) = { <. a , b >. \| ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } ) : No typesetting found for \|- ( ph -> ( R ~RL S ) = { <. a , b >. \| ( ( a e. ( B X. S ) /\ b e. ( B X. S ) ) /\ E. t e. S ( t .x. ( ( ( 1st ` a ) .x. ( 2nd ` b ) ) .- ( ( 1st ` b ) .x. ( 2nd ` a ) ) ) ) = .0. ) } ) with typecode \|-
28	2 27	eqtrid	$⊢ φ \to \underset{˙}{\sim} = \{⟨a, b⟩ \| ((a \in (B \times S) \land b \in (B \times S)) \land \exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0})\}$
29		simprl	$⊢ (φ \land (a = U \land b = V)) \to a = U$
30	29	fveq2d	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (a) = 1^{st} (U)$
31	7	fveq2d	$⊢ φ \to 1^{st} (U) = 1^{st} (⟨E, G⟩)$
32		op1stg	$⊢ (E \in B \land G \in S) \to 1^{st} (⟨E, G⟩) = E$
33	9 11 32	syl2anc	$⊢ φ \to 1^{st} (⟨E, G⟩) = E$
34	31 33	eqtrd	$⊢ φ \to 1^{st} (U) = E$
35	34	adantr	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (U) = E$
36	30 35	eqtrd	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (a) = E$
37		simprr	$⊢ (φ \land (a = U \land b = V)) \to b = V$
38	37	fveq2d	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (b) = 2^{nd} (V)$
39	8	fveq2d	$⊢ φ \to 2^{nd} (V) = 2^{nd} (⟨F, H⟩)$
40		op2ndg	$⊢ (F \in B \land H \in S) \to 2^{nd} (⟨F, H⟩) = H$
41	10 12 40	syl2anc	$⊢ φ \to 2^{nd} (⟨F, H⟩) = H$
42	39 41	eqtrd	$⊢ φ \to 2^{nd} (V) = H$
43	42	adantr	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (V) = H$
44	38 43	eqtrd	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (b) = H$
45	36 44	oveq12d	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b) = E \underset{˙}{\cdot} H$
46	37	fveq2d	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (b) = 1^{st} (V)$
47	8	fveq2d	$⊢ φ \to 1^{st} (V) = 1^{st} (⟨F, H⟩)$
48		op1stg	$⊢ (F \in B \land H \in S) \to 1^{st} (⟨F, H⟩) = F$
49	10 12 48	syl2anc	$⊢ φ \to 1^{st} (⟨F, H⟩) = F$
50	47 49	eqtrd	$⊢ φ \to 1^{st} (V) = F$
51	50	adantr	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (V) = F$
52	46 51	eqtrd	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (b) = F$
53	29	fveq2d	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (a) = 2^{nd} (U)$
54	7	fveq2d	$⊢ φ \to 2^{nd} (U) = 2^{nd} (⟨E, G⟩)$
55		op2ndg	$⊢ (E \in B \land G \in S) \to 2^{nd} (⟨E, G⟩) = G$
56	9 11 55	syl2anc	$⊢ φ \to 2^{nd} (⟨E, G⟩) = G$
57	54 56	eqtrd	$⊢ φ \to 2^{nd} (U) = G$
58	57	adantr	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (U) = G$
59	53 58	eqtrd	$⊢ (φ \land (a = U \land b = V)) \to 2^{nd} (a) = G$
60	52 59	oveq12d	$⊢ (φ \land (a = U \land b = V)) \to 1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a) = F \underset{˙}{\cdot} G$
61	45 60	oveq12d	$⊢ (φ \land (a = U \land b = V)) \to (1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a)) = (E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)$
62	61	oveq2d	$⊢ (φ \land (a = U \land b = V)) \to t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G))$
63	62	eqeq1d	$⊢ (φ \land (a = U \land b = V)) \to (t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0})$
64	63	rexbidv	$⊢ (φ \land (a = U \land b = V)) \to (\exists t \in S t \underset{˙}{\cdot} ((1^{st} (a) \underset{˙}{\cdot} 2^{nd} (b)) \underset{˙}{-} (1^{st} (b) \underset{˙}{\cdot} 2^{nd} (a))) = \underset{˙}{0} \leftrightarrow \exists t \in S t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0})$
65	28 64	brab2d	$⊢ φ \to (U \underset{˙}{\sim} V \leftrightarrow ((U \in (B \times S) \land V \in (B \times S)) \land \exists t \in S t \underset{˙}{\cdot} ((E \underset{˙}{\cdot} H) \underset{˙}{-} (F \underset{˙}{\cdot} G)) = \underset{˙}{0}))$
66	24 65	mpbird	$⊢ φ \to U \underset{˙}{\sim} V$

Metamath Proof Explorer

Theorem erlbrd

Proof