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 e. LMod /\ V e. ~P B ) -> ( M LinCo V ) = ( ( LSpan ` M ) ` V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lspeqvlco.b | |- B = ( Base ` M ) |
|
| 2 | 1 | lcosslsp | |- ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) C_ ( ( LSpan ` M ) ` V ) ) |
| 3 | 1 | lspsslco | |- ( ( M e. LMod /\ V e. ~P B ) -> ( ( LSpan ` M ) ` V ) C_ ( M LinCo V ) ) |
| 4 | 2 3 | eqssd | |- ( ( M e. LMod /\ V e. ~P B ) -> ( M LinCo V ) = ( ( LSpan ` M ) ` V ) ) |