# Metamath Proof Explorer

## Theorem frlmlmod

Description: The free module is a module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypothesis frlmval.f
`|- F = ( R freeLMod I )`
Assertion frlmlmod
`|- ( ( R e. Ring /\ I e. W ) -> F e. LMod )`

### Proof

Step Hyp Ref Expression
1 frlmval.f
` |-  F = ( R freeLMod I )`
2 1 frlmval
` |-  ( ( R e. Ring /\ I e. W ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )`
3 simpr
` |-  ( ( R e. Ring /\ I e. W ) -> I e. W )`
4 simpl
` |-  ( ( R e. Ring /\ I e. W ) -> R e. Ring )`
5 rlmlmod
` |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )`
` |-  ( ( R e. Ring /\ I e. W ) -> ( ringLMod ` R ) e. LMod )`
7 fconst6g
` |-  ( ( ringLMod ` R ) e. LMod -> ( I X. { ( ringLMod ` R ) } ) : I --> LMod )`
8 6 7 syl
` |-  ( ( R e. Ring /\ I e. W ) -> ( I X. { ( ringLMod ` R ) } ) : I --> LMod )`
9 fvex
` |-  ( ringLMod ` R ) e. _V`
10 9 fvconst2
` |-  ( i e. I -> ( ( I X. { ( ringLMod ` R ) } ) ` i ) = ( ringLMod ` R ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( ( I X. { ( ringLMod ` R ) } ) ` i ) = ( ringLMod ` R ) )`
12 11 fveq2d
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( Scalar ` ( ( I X. { ( ringLMod ` R ) } ) ` i ) ) = ( Scalar ` ( ringLMod ` R ) ) )`
13 rlmsca
` |-  ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> R = ( Scalar ` ( ringLMod ` R ) ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( Scalar ` ( ( I X. { ( ringLMod ` R ) } ) ` i ) ) = R )`
` |-  ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( R (+)m ( I X. { ( ringLMod ` R ) } ) )`
` |-  ( ( R e. Ring /\ I e. W ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) e. LMod )`
` |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )`