Metamath Proof Explorer


Theorem reldmresv

Description: The scalar restriction is a proper operator, so it can be used with ovprc1 . (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion reldmresv Reldom𝑣

Proof

Step Hyp Ref Expression
1 df-resv 𝑣=yV,xVifBaseScalaryxyysSetScalarndxScalary𝑠x
2 1 reldmmpo Reldom𝑣