erldi

Description: Main property of the ring localization equivalence 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 ‘ 𝑅 )
	erldi.4	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )
Assertion	erldi	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 )

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		erldi.4	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )
8		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
9		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) }
10	1 4 5 6 8 9 3	erlval	⊢ ( 𝜑 → ( 𝑅 ~_RL 𝑆 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } )
11	2 10	eqtrid	⊢ ( 𝜑 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } )
12		simpl	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑎 = 𝑈 )
13	12	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑈 ) )
14		simpr	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑏 = 𝑉 )
15	14	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ 𝑉 ) )
16	13 15	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) = ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) )
17	14	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ 𝑉 ) )
18	12	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑈 ) )
19	17 18	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) )
20	16 19	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) = ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) )
22	21	eqeq1d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ↔ ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 ) )
23	22	rexbidv	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 ) )
25	11 24	brab2d	⊢ ( 𝜑 → ( 𝑈 ∼ 𝑉 ↔ ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 ) ) )
26	7 25	mpbid	⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 ) )
27	26	simprd	⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑈 ) · ( 2^nd ‘ 𝑉 ) ) − ( ( 1^st ‘ 𝑉 ) · ( 2^nd ‘ 𝑈 ) ) ) ) = 0 )

Metamath Proof Explorer

Theorem erldi

Proof