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	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	lspeqlco	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) = ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lspeqvlco.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2	1	lcosslsp	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) ⊆ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) )
3	1	lspsslco	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ⊆ ( 𝑀 LinCo 𝑉 ) )
4	2 3	eqssd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 LinCo 𝑉 ) = ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) )