This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
6 5 adantr 
 |-  ( ( 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 ) )
11 10 adantl 
 |-  ( ( ( 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 ) ) )
14 13 ad2antrr 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
15 12 14 eqtr4d 
 |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( Scalar ` ( ( I X. { ( ringLMod ` R ) } ) ` i ) ) = R )
16 eqid 
 |-  ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) = ( R (+)m ( I X. { ( ringLMod ` R ) } ) )
17 3 4 8 15 16 dsmmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) e. LMod )
18 2 17 eqeltrd 
 |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )