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 ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
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 )