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 e. _V , s e. _V |-> [_ ( .r ` r ) / x ]_ [_ ( ( Base ` r ) X. s ) / w ]_ ( ( ( { <. ( Base ` ndx ) , w >. , <. ( +g ` ndx ) , ( a e. w , b e. w |-> <. ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( +g ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. , <. ( .r ` ndx ) , ( a e. w , b e. w |-> <. ( ( 1st ` a ) x ( 1st ` b ) ) , ( ( 2nd ` a ) x ( 2nd ` b ) ) >. ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` r ) ) , a e. w |-> <. ( k ( .s ` r ) ( 1st ` a ) ) , ( 2nd ` a ) >. ) >. , <. ( .i ` ndx ) , (/) >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopSet ` r ) tX ( ( TopSet ` r ) |`t s ) ) >. , <. ( le ` ndx ) , { <. a , b >. | ( ( a e. w /\ b e. w ) /\ ( ( 1st ` a ) x ( 2nd ` b ) ) ( le ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) } >. , <. ( dist ` ndx ) , ( a e. w , b e. w |-> ( ( ( 1st ` a ) x ( 2nd ` b ) ) ( dist ` r ) ( ( 1st ` b ) x ( 2nd ` a ) ) ) ) >. } ) /s ( r ~RL s ) ) )
2	1	reldmmpo	|- Rel dom RLocal