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 )