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	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	dsmmlss.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
	dsmmlss.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
	dsmmlss.k	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
	dsmmlmod.c	⊢ 𝐶 = ( 𝑆 ⊕m 𝑅 )
Assertion	dsmmlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		dsmmlss.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
2		dsmmlss.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
3		dsmmlss.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
4		dsmmlss.k	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑥 ) ) = 𝑆 )
5		dsmmlmod.c	⊢ 𝐶 = ( 𝑆 ⊕m 𝑅 )
6		eqid	⊢ ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs 𝑅 )
7	6 2 1 3 4	prdslmodd	⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) ∈ LMod )
8		eqid	⊢ ( LSubSp ‘ ( 𝑆 Xs 𝑅 ) ) = ( LSubSp ‘ ( 𝑆 Xs 𝑅 ) )
9		eqid	⊢ ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
10	1 2 3 4 6 8 9	dsmmlss	⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ∈ ( LSubSp ‘ ( 𝑆 Xs 𝑅 ) ) )
11	9	dsmmval2	⊢ ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
12	5 11	eqtri	⊢ 𝐶 = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
13	12 8	lsslmod	⊢ ( ( ( 𝑆 Xs 𝑅 ) ∈ LMod ∧ ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ∈ ( LSubSp ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝐶 ∈ LMod )
14	7 10 13	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ LMod )