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 = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( .r𝑟 ) / 𝑥 ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑎𝑤 , 𝑏𝑤 ↦ ⟨ ( ( ( 1st𝑎 ) 𝑥 ( 2nd𝑏 ) ) ( +g𝑟 ) ( ( 1st𝑏 ) 𝑥 ( 2nd𝑎 ) ) ) , ( ( 2nd𝑎 ) 𝑥 ( 2nd𝑏 ) ) ⟩ ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑎𝑤 , 𝑏𝑤 ↦ ⟨ ( ( 1st𝑎 ) 𝑥 ( 1st𝑏 ) ) , ( ( 2nd𝑎 ) 𝑥 ( 2nd𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎𝑤 ↦ ⟨ ( 𝑘 ( ·𝑠𝑟 ) ( 1st𝑎 ) ) , ( 2nd𝑎 ) ⟩ ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×t ( ( TopSet ‘ 𝑟 ) ↾t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎𝑤𝑏𝑤 ) ∧ ( ( 1st𝑎 ) 𝑥 ( 2nd𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1st𝑏 ) 𝑥 ( 2nd𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎𝑤 , 𝑏𝑤 ↦ ( ( ( 1st𝑎 ) 𝑥 ( 2nd𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1st𝑏 ) 𝑥 ( 2nd𝑎 ) ) ) ) ⟩ } ) /s ( 𝑟 ~RL 𝑠 ) ) )
2 1 reldmmpo Rel dom RLocal