Metamath Proof Explorer

Theorem lspeqlco

Description: Equivalence of aspan of a set of vectors of a left module defined as the intersection of all linear subspaces which each contain every vector in that set (see df-lsp ) and as the set of all linear combinations of the vectors of the set with finite support. (Contributed by AV, 20-Apr-2019)

Ref Expression
Hypothesis lspeqvlco.b ⊢ B = Base M
Assertion lspeqlco ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M LinCo V = LSpan ⁡ M ⁡ V

Proof

Step Hyp Ref Expression
1 lspeqvlco.b ⊢ B = Base M
2 1 lcosslsp ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M LinCo V ⊆ LSpan ⁡ M ⁡ V
3 1 lspsslco ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → LSpan ⁡ M ⁡ V ⊆ M LinCo V
4 2 3 eqssd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M LinCo V = LSpan ⁡ M ⁡ V