Metamath Proof Explorer

Theorem lincolss

Description: According to the statement in Lang p. 129, the set ( LSubSpM ) of all linear combinations of a set of vectors V is a submodule (_generated_ by V) of the module M. The elements of V are called generators of ( LSubSpM ) . (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lincolss ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → M LinCo V ∈ LSubSp ⁡ M

Proof

Step Hyp Ref Expression
1 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → Scalar ⁡ M = Scalar ⁡ M
2 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → Base Scalar ⁡ M = Base Scalar ⁡ M
3 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → Base M = Base M
4 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → + M = + M
5 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → ⋅ M = ⋅ M
6 eqidd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → LSubSp ⁡ M = LSubSp ⁡ M
7 eqid ⊢ Base M = Base M
8 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
9 eqid ⊢ Base Scalar ⁡ M = Base Scalar ⁡ M
10 7 8 9 lcoval ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → v ∈ M LinCo V ↔ v ∈ Base M ∧ ∃ s ∈ Base Scalar ⁡ M V finSupp 0 Scalar ⁡ M ⁡ s ∧ v = s linC ⁡ M V
11 simpl ⊢ v ∈ Base M ∧ ∃ s ∈ Base Scalar ⁡ M V finSupp 0 Scalar ⁡ M ⁡ s ∧ v = s linC ⁡ M V → v ∈ Base M
12 10 11 syl6bi ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → v ∈ M LinCo V → v ∈ Base M
13 12 ssrdv ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → M LinCo V ⊆ Base M
14 lcoel0 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → 0 M ∈ M LinCo V
15 14 ne0d ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → M LinCo V ≠ ∅
16 eqid ⊢ ⋅ M = ⋅ M
17 eqid ⊢ + M = + M
18 16 9 17 lincsumscmcl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ x ∈ Base Scalar ⁡ M ∧ a ∈ M LinCo V ∧ b ∈ M LinCo V → x ⋅ M a + M b ∈ M LinCo V
19 1 2 3 4 5 6 13 15 18 islssd ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → M LinCo V ∈ LSubSp ⁡ M