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 e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) e. ( LSubSp ` M ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( Scalar ` M ) = ( Scalar ` M ) )
2 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) ) )
3 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( Base ` M ) = ( Base ` M ) )
4 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( +g ` M ) = ( +g ` M ) )
5 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( .s ` M ) = ( .s ` M ) )
6 eqidd 
 |-  ( ( M e. LMod /\ V e. ~P ( 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 e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. ( M LinCo V ) <-> ( v e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( s ( linC ` M ) V ) ) ) ) )
11 simpl 
 |-  ( ( v e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( s ( linC ` M ) V ) ) ) -> v e. ( Base ` M ) )
12 10 11 syl6bi 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. ( M LinCo V ) -> v e. ( Base ` M ) ) )
13 12 ssrdv 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) C_ ( Base ` M ) )
14 lcoel0 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( 0g ` M ) e. ( M LinCo V ) )
15 14 ne0d 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) =/= (/) )
16 eqid 
 |-  ( .s ` M ) = ( .s ` M )
17 eqid 
 |-  ( +g ` M ) = ( +g ` M )
18 16 9 17 lincsumscmcl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ a e. ( M LinCo V ) /\ b e. ( M LinCo V ) ) ) -> ( ( x ( .s ` M ) a ) ( +g ` M ) b ) e. ( M LinCo V ) )
19 1 2 3 4 5 6 13 15 18 islssd 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo V ) e. ( LSubSp ` M ) )