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 ⊢ φ → I ∈ W
dsmmlss.s ⊢ φ → S ∈ Ring
dsmmlss.r ⊢ φ → R : I ⟶ LMod
dsmmlss.k ⊢ φ ∧ x ∈ I → Scalar ⁡ R ⁡ x = S
dsmmlmod.c ⊢ C = S ⊕ m R
Assertion dsmmlmod ⊢ φ → C ∈ LMod

Proof

Step Hyp Ref Expression
1 dsmmlss.i ⊢ φ → I ∈ W
2 dsmmlss.s ⊢ φ → S ∈ Ring
3 dsmmlss.r ⊢ φ → R : I ⟶ LMod
4 dsmmlss.k ⊢ φ ∧ x ∈ I → Scalar ⁡ R ⁡ x = S
5 dsmmlmod.c ⊢ C = S ⊕ m R
6 eqid ⊢ S ⨉ 𝑠 R = S ⨉ 𝑠 R
7 6 2 1 3 4 prdslmodd ⊢ φ → S ⨉ 𝑠 R ∈ LMod
8 eqid ⊢ LSubSp ⁡ S ⨉ 𝑠 R = LSubSp ⁡ S ⨉ 𝑠 R
9 eqid ⊢ Base S ⊕ m R = Base S ⊕ m R
10 1 2 3 4 6 8 9 dsmmlss ⊢ φ → Base S ⊕ m R ∈ LSubSp ⁡ S ⨉ 𝑠 R
11 9 dsmmval2 ⊢ S ⊕ m R = S ⨉ 𝑠 R ↾ 𝑠 Base S ⊕ m R
12 5 11 eqtri ⊢ C = S ⨉ 𝑠 R ↾ 𝑠 Base S ⊕ m R
13 12 8 lsslmod ⊢ S ⨉ 𝑠 R ∈ LMod ∧ Base S ⊕ m R ∈ LSubSp ⁡ S ⨉ 𝑠 R → C ∈ LMod
14 7 10 13 syl2anc ⊢ φ → C ∈ LMod