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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	erlcl1.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	erlcl1.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	erldi.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	erldi.2	⊢ · = ( ._r ‘ 𝑅 )
	erldi.3	⊢ − = ( -_g ‘ 𝑅 )
	erlbrd.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐸 , 𝐺 ⟩ )
	erlbrd.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝐹 , 𝐻 ⟩ )
	erlbrd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	erlbrd.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	erlbrd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	erlbrd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
	erlbrd.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	erlbrd.2	⊢ ( 𝜑 → ( 𝑇 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 )
Assertion	erlbrd	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		erlcl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		erlcl1.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
3		erlcl1.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4		erldi.1	⊢ 0 = ( 0_g ‘ 𝑅 )
5		erldi.2	⊢ · = ( ._r ‘ 𝑅 )
6		erldi.3	⊢ − = ( -_g ‘ 𝑅 )
7		erlbrd.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐸 , 𝐺 ⟩ )
8		erlbrd.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝐹 , 𝐻 ⟩ )
9		erlbrd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
10		erlbrd.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11		erlbrd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
12		erlbrd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
13		erlbrd.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
14		erlbrd.2	⊢ ( 𝜑 → ( 𝑇 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 )
15	9 11	opelxpd	⊢ ( 𝜑 → ⟨ 𝐸 , 𝐺 ⟩ ∈ ( 𝐵 × 𝑆 ) )
16	7 15	eqeltrd	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐵 × 𝑆 ) )
17	10 12	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐻 ⟩ ∈ ( 𝐵 × 𝑆 ) )
18	8 17	eqeltrd	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐵 × 𝑆 ) )
19	16 18	jca	⊢ ( 𝜑 → ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑡 = 𝑇 ) → 𝑡 = 𝑇 )
21	20	oveq1d	⊢ ( ( 𝜑 ∧ 𝑡 = 𝑇 ) → ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = ( 𝑇 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) )
22	21	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑡 = 𝑇 ) → ( ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ↔ ( 𝑇 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ) )
23	13 22 14	rspcedvd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 )
24	19 23	jca	⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ) )
25		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
26		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) }
27	1 4 5 6 25 26 3	erlval	⊢ ( 𝜑 → ( 𝑅 ~_RL 𝑆 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } )
28	2 27	eqtrid	⊢ ( 𝜑 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } )
29		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → 𝑎 = 𝑈 )
30	29	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑈 ) )
31	7	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) = ( 1^st ‘ ⟨ 𝐸 , 𝐺 ⟩ ) )
32		op1stg	⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆 ) → ( 1^st ‘ ⟨ 𝐸 , 𝐺 ⟩ ) = 𝐸 )
33	9 11 32	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐸 , 𝐺 ⟩ ) = 𝐸 )
34	31 33	eqtrd	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) = 𝐸 )
35	34	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑈 ) = 𝐸 )
36	30 35	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑎 ) = 𝐸 )
37		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → 𝑏 = 𝑉 )
38	37	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ 𝑉 ) )
39	8	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑉 ) = ( 2^nd ‘ ⟨ 𝐹 , 𝐻 ⟩ ) )
40		op2ndg	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆 ) → ( 2^nd ‘ ⟨ 𝐹 , 𝐻 ⟩ ) = 𝐻 )
41	10 12 40	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐻 ⟩ ) = 𝐻 )
42	39 41	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑉 ) = 𝐻 )
43	42	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑉 ) = 𝐻 )
44	38 43	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑏 ) = 𝐻 )
45	36 44	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) = ( 𝐸 · 𝐻 ) )
46	37	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ 𝑉 ) )
47	8	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝑉 ) = ( 1^st ‘ ⟨ 𝐹 , 𝐻 ⟩ ) )
48		op1stg	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐻 ∈ 𝑆 ) → ( 1^st ‘ ⟨ 𝐹 , 𝐻 ⟩ ) = 𝐹 )
49	10 12 48	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐻 ⟩ ) = 𝐹 )
50	47 49	eqtrd	⊢ ( 𝜑 → ( 1^st ‘ 𝑉 ) = 𝐹 )
51	50	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑉 ) = 𝐹 )
52	46 51	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 1^st ‘ 𝑏 ) = 𝐹 )
53	29	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑈 ) )
54	7	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = ( 2^nd ‘ ⟨ 𝐸 , 𝐺 ⟩ ) )
55		op2ndg	⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝐺 ∈ 𝑆 ) → ( 2^nd ‘ ⟨ 𝐸 , 𝐺 ⟩ ) = 𝐺 )
56	9 11 55	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐸 , 𝐺 ⟩ ) = 𝐺 )
57	54 56	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = 𝐺 )
58	57	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑈 ) = 𝐺 )
59	53 58	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 2^nd ‘ 𝑎 ) = 𝐺 )
60	52 59	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) = ( 𝐹 · 𝐺 ) )
61	45 60	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) = ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) )
62	61	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) )
63	62	eqeq1d	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ↔ ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ) )
64	63	rexbidv	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ) )
65	28 64	brab2d	⊢ ( 𝜑 → ( 𝑈 ∼ 𝑉 ↔ ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( 𝐸 · 𝐻 ) − ( 𝐹 · 𝐺 ) ) ) = 0 ) ) )
66	24 65	mpbird	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )

Metamath Proof Explorer

Theorem erlbrd

Proof