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	$$⊢\phi \to I\in W$$
	dsmmlss.s	$$⊢\phi \to S\in \mathrm{Ring}$$
	dsmmlss.r	$$⊢\phi \to R:I⟶\mathrm{LMod}$$
	dsmmlss.k	$$⊢\left(\phi \wedge x\in I\right)\to \mathrm{Scalar}\left(R\left(x\right)\right)=S$$
	dsmmlmod.c	$$⊢C=S{\oplus }_{m}R$$
Assertion	dsmmlmod	$$⊢\phi \to C\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		dsmmlss.i	$$⊢\phi \to I\in W$$
2		dsmmlss.s	$$⊢\phi \to S\in \mathrm{Ring}$$
3		dsmmlss.r	$$⊢\phi \to R:I⟶\mathrm{LMod}$$
4		dsmmlss.k	$$⊢\left(\phi \wedge x\in I\right)\to \mathrm{Scalar}\left(R\left(x\right)\right)=S$$
5		dsmmlmod.c	$$⊢C=S{\oplus }_{m}R$$
6		eqid	$$⊢S{⨉}_{𝑠}R=S{⨉}_{𝑠}R$$
7	6 2 1 3 4	prdslmodd	$$⊢\phi \to S{⨉}_{𝑠}R\in \mathrm{LMod}$$
8		eqid	$$⊢\mathrm{LSubSp}\left(S{⨉}_{𝑠}R\right)=\mathrm{LSubSp}\left(S{⨉}_{𝑠}R\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}={\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}$$
10	1 2 3 4 6 8 9	dsmmlss	$$⊢\phi \to {\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}\in \mathrm{LSubSp}\left(S{⨉}_{𝑠}R\right)$$
11	9	dsmmval2	$$⊢S{\oplus }_{m}R=\left(S{⨉}_{𝑠}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}$$
12	5 11	eqtri	$$⊢C=\left(S{⨉}_{𝑠}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}$$
13	12 8	lsslmod	$$⊢\left(S{⨉}_{𝑠}R\in \mathrm{LMod}\wedge {\mathrm{Base}}_{\left(S{\oplus }_{m}R\right)}\in \mathrm{LSubSp}\left(S{⨉}_{𝑠}R\right)\right)\to C\in \mathrm{LMod}$$
14	7 10 13	syl2anc	$$⊢\phi \to C\in \mathrm{LMod}$$