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 ‘ 𝑎 ) ‘ ( Base ‘ 𝑎 ) ) ∈ V
2		df-rgmod	⊢ ringLMod = ( 𝑎 ∈ V ↦ ( ( subringAlg ‘ 𝑎 ) ‘ ( Base ‘ 𝑎 ) ) )
3	1 2	fnmpti	⊢ ringLMod Fn V