This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldmrloc

Description: Ring localization is a proper operator, so it can be used with ovprc1 . (Contributed by Thierry Arnoux, 10-May-2025)

Ref Expression
Assertion reldmrloc ⊢ Rel ⁡ dom ⁡ RLocal

Proof

Step Hyp Ref Expression
1 df-rloc ⊢ RLocal = r ∈ V , s ∈ V ⟼ ⦋ ⋅ r / x⦌ ⦋ Base r × s / w⦌ Base ndx w + ndx a ∈ w , b ∈ w ⟼ 1 st ⁡ a x 2 nd ⁡ b + r 1 st ⁡ b x 2 nd ⁡ a 2 nd ⁡ a x 2 nd ⁡ b ⋅ ndx a ∈ w , b ∈ w ⟼ 1 st ⁡ a x 1 st ⁡ b 2 nd ⁡ a x 2 nd ⁡ b ∪ Scalar ⁡ ndx Scalar ⁡ r ⋅ ndx k ∈ Base Scalar ⁡ r , a ∈ w ⟼ k ⋅ r 1 st ⁡ a 2 nd ⁡ a ⋅ 𝑖 ⁡ ndx ∅ ∪ TopSet ⁡ ndx TopSet ⁡ r × t TopSet ⁡ r ↾ 𝑡 s ≤ ndx a b | a ∈ w ∧ b ∈ w ∧ 1 st ⁡ a x 2 nd ⁡ b ≤ r 1 st ⁡ b x 2 nd ⁡ a dist ⁡ ndx a ∈ w , b ∈ w ⟼ 1 st ⁡ a x 2 nd ⁡ b dist ⁡ r 1 st ⁡ b x 2 nd ⁡ a / 𝑠 r ~RL s
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ RLocal