Metamath Proof Explorer

Theorem lincellss

Description: A linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Assertion lincellss 
|- ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( F ( linC ` M ) V ) e. S ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> M e. LMod )
2 simprl 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
3 ssexg 
 |-  ( ( V C_ S /\ S e. ( LSubSp ` M ) ) -> V e. _V )
4 3 ancoms 
 |-  ( ( S e. ( LSubSp ` M ) /\ V C_ S ) -> V e. _V )
5 eqid 
 |-  ( Base ` M ) = ( Base ` M )
6 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
7 5 6 lssss 
 |-  ( S e. ( LSubSp ` M ) -> S C_ ( Base ` M ) )
8 sstr 
 |-  ( ( V C_ S /\ S C_ ( Base ` M ) ) -> V C_ ( Base ` M ) )
9 elpwg 
 |-  ( V e. _V -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
10 8 9 syl5ibrcom 
 |-  ( ( V C_ S /\ S C_ ( Base ` M ) ) -> ( V e. _V -> V e. ~P ( Base ` M ) ) )
11 10 expcom 
 |-  ( S C_ ( Base ` M ) -> ( V C_ S -> ( V e. _V -> V e. ~P ( Base ` M ) ) ) )
12 7 11 syl 
 |-  ( S e. ( LSubSp ` M ) -> ( V C_ S -> ( V e. _V -> V e. ~P ( Base ` M ) ) ) )
13 12 imp 
 |-  ( ( S e. ( LSubSp ` M ) /\ V C_ S ) -> ( V e. _V -> V e. ~P ( Base ` M ) ) )
14 4 13 mpd 
 |-  ( ( S e. ( LSubSp ` M ) /\ V C_ S ) -> V e. ~P ( Base ` M ) )
15 14 3adant1 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> V e. ~P ( Base ` M ) )
16 15 adantr 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> V e. ~P ( Base ` M ) )
17 lincval 
 |-  ( ( M e. LMod /\ F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
18 1 2 16 17 syl3anc 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
19 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
20 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
21 6 19 20 gsumlsscl 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. S ) )
22 21 imp 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. S )
23 18 22 eqeltrd 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> ( F ( linC ` M ) V ) e. S )
24 23 ex 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ F finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( F ( linC ` M ) V ) e. S ) )