Theorem dsmmlmod

Description: The direct sum of a family of modules is a module. See also the remark in Lang p. 128. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmlss.i	|- ( ph -> I e. W )
	dsmmlss.s	|- ( ph -> S e. Ring )
	dsmmlss.r	|- ( ph -> R : I --> LMod )
	dsmmlss.k	|- ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = S )
	dsmmlmod.c	|- C = ( S (+)m R )
Assertion	dsmmlmod	|- ( ph -> C e. LMod )

Proof

Step	Hyp	Ref	Expression
1		dsmmlss.i	|- ( ph -> I e. W )
2		dsmmlss.s	|- ( ph -> S e. Ring )
3		dsmmlss.r	|- ( ph -> R : I --> LMod )
4		dsmmlss.k	|- ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = S )
5		dsmmlmod.c	|- C = ( S (+)m R )
6		eqid	|- ( S Xs_ R ) = ( S Xs_ R )
7	6 2 1 3 4	prdslmodd	|- ( ph -> ( S Xs_ R ) e. LMod )
8		eqid	|- ( LSubSp ` ( S Xs_ R ) ) = ( LSubSp ` ( S Xs_ R ) )
9		eqid	|- ( Base ` ( S (+)m R ) ) = ( Base ` ( S (+)m R ) )
10	1 2 3 4 6 8 9	dsmmlss	|- ( ph -> ( Base ` ( S (+)m R ) ) e. ( LSubSp ` ( S Xs_ R ) ) )
11	9	dsmmval2	|- ( S (+)m R ) = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) )
12	5 11	eqtri	|- C = ( ( S Xs_ R ) |`s ( Base ` ( S (+)m R ) ) )
13	12 8	lsslmod	|- ( ( ( S Xs_ R ) e. LMod /\ ( Base ` ( S (+)m R ) ) e. ( LSubSp ` ( S Xs_ R ) ) ) -> C e. LMod )
14	7 10 13	syl2anc	|- ( ph -> C e. LMod )