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

Metamath Proof Explorer

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 )