Database
BASIC ALGEBRAIC STRUCTURES
Ideals
The subring algebra; ideals
rlmfn
Next ⟩
rlmval
Metamath Proof Explorer
Ascii
Unicode
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