Metamath Proof Explorer


Theorem rlmfn

Description: ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014)

Ref Expression
Assertion rlmfn ringLMod Fn V

Proof

Step Hyp Ref Expression
1 fvex subringAlg a Base a V
2 df-rgmod ringLMod = a V subringAlg a Base a
3 1 2 fnmpti ringLMod Fn V