erlcl2

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

	Ref	Expression
Hypotheses	erlcl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	erlcl1.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	erlcl1.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	erlcl1.1	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )
Assertion	erlcl2	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐵 × 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		erlcl1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		erlcl1.e	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
3		erlcl1.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4		erlcl1.1	⊢ ( 𝜑 → 𝑈 ∼ 𝑉 )
5		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
6		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
7		eqid	⊢ ( -_g ‘ 𝑅 ) = ( -_g ‘ 𝑅 )
8		eqid	⊢ ( 𝐵 × 𝑆 ) = ( 𝐵 × 𝑆 )
9		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) }
10	1 5 6 7 8 9 3	erlval	⊢ ( 𝜑 → ( 𝑅 ~_RL 𝑆 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) } )
11	2 10	eqtrid	⊢ ( 𝜑 → ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑏 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) } )
12		simpl	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑎 = 𝑈 )
13	12	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑈 ) )
14		simpr	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → 𝑏 = 𝑉 )
15	14	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 2^nd ‘ 𝑏 ) = ( 2^nd ‘ 𝑉 ) )
16	13 15	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) = ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) )
17	14	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ 𝑉 ) )
18	12	fveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑈 ) )
19	17 18	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) )
20	16 19	oveq12d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) = ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) )
21	20	oveq2d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) )
22	21	eqeq1d	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ↔ ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) )
23	22	rexbidv	⊢ ( ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝑈 ∧ 𝑏 = 𝑉 ) ) → ( ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑎 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑅 ) ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) )
25	11 24	brab2d	⊢ ( 𝜑 → ( 𝑈 ∼ 𝑉 ↔ ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) ) )
26	4 25	mpbid	⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝐵 × 𝑆 ) ∧ 𝑉 ∈ ( 𝐵 × 𝑆 ) ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 ( ._r ‘ 𝑅 ) ( ( ( 1^st ‘ 𝑈 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑉 ) ) ( -_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑉 ) ( ._r ‘ 𝑅 ) ( 2^nd ‘ 𝑈 ) ) ) ) = ( 0_g ‘ 𝑅 ) ) )
27	26	simplrd	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐵 × 𝑆 ) )

Metamath Proof Explorer

Theorem erlcl2

Proof