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	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{RLocal}$$

Proof

Step	Hyp	Ref	Expression
1		df-rloc	$$⊢\mathrm{RLocal}=\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋{\cdot }_r/x⦌⦋\left({\mathrm{Base}}_r\times s\right)/w⦌\left(\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},w⟩,⟨{+}_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){+}_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(a\in w,b\in w⟼⟨1^{st}\left(a\right)x{1}^{st}\left(b\right),2^{nd}\left(a\right)x{2}^{nd}\left(b\right)⟩\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(r\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(r\right)},a\in w⟼⟨k{\cdot }_r{1}^{st}\left(a\right),2^{nd}\left(a\right)⟩\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(r\right){\times }_t\left(\mathrm{TopSet}\left(r\right){\upharpoonright }_{𝑡}s\right)⟩,⟨{\le }_{\mathrm{ndx}},\left\{⟨a,b⟩|\left(\left(a\in w\wedge b\in w\right)\wedge \left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right){\le }_r\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)\right\}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(a\in w,b\in w⟼\left(1^{st}\left(a\right)x{2}^{nd}\left(b\right)\right)\mathrm{dist}\left(r\right)\left(1^{st}\left(b\right)x{2}^{nd}\left(a\right)\right)\right)⟩\right\}\right){/}_{𝑠}\left(r{~}_{\mathrm{RL}}s\right)\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{RLocal}$$