Metamath Proof Explorer

Theorem ellcoellss

Description: Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion ellcoellss 
|- ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> A. x e. ( M LinCo V ) x e. S )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> M e. LMod )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
4 2 3 lssss 
 |-  ( S e. ( LSubSp ` M ) -> S C_ ( Base ` M ) )
5 4 3ad2ant2 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> S C_ ( Base ` M ) )
6 sstr 
 |-  ( ( V C_ S /\ S C_ ( Base ` M ) ) -> V C_ ( Base ` M ) )
7 fvex 
 |-  ( Base ` M ) e. _V
8 7 ssex 
 |-  ( V C_ ( Base ` M ) -> V e. _V )
9 elpwg 
 |-  ( V e. _V -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
10 9 biimprd 
 |-  ( V e. _V -> ( V C_ ( Base ` M ) -> V e. ~P ( Base ` M ) ) )
11 8 10 mpcom 
 |-  ( V C_ ( Base ` M ) -> V e. ~P ( Base ` M ) )
12 6 11 syl 
 |-  ( ( V C_ S /\ S C_ ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
13 12 ex 
 |-  ( V C_ S -> ( S C_ ( Base ` M ) -> V e. ~P ( Base ` M ) ) )
14 13 3ad2ant3 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( S C_ ( Base ` M ) -> V e. ~P ( Base ` M ) ) )
15 5 14 mpd 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> V e. ~P ( Base ` M ) )
16 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
17 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
18 2 16 17 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( x e. ( M LinCo V ) <-> ( x e. ( Base ` M ) /\ E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) ) ) )
19 1 15 18 syl2anc 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( x e. ( M LinCo V ) <-> ( x e. ( Base ` M ) /\ E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) ) ) )
20 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 ) )
21 20 imp 
 |-  ( ( ( 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 )
22 eleq1 
 |-  ( x = ( f ( linC ` M ) V ) -> ( x e. S <-> ( f ( linC ` M ) V ) e. S ) )
23 21 22 imbitrrid 
 |-  ( x = ( f ( linC ` M ) V ) -> ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ f finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> x e. S ) )
24 23 expd 
 |-  ( x = ( f ( linC ` M ) V ) -> ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ f finSupp ( 0g ` ( Scalar ` M ) ) ) -> x e. S ) ) )
25 24 com12 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( x = ( f ( linC ` M ) V ) -> ( ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ f finSupp ( 0g ` ( Scalar ` M ) ) ) -> x e. S ) ) )
26 25 adantr 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ x e. ( Base ` M ) ) -> ( x = ( f ( linC ` M ) V ) -> ( ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ f finSupp ( 0g ` ( Scalar ` M ) ) ) -> x e. S ) ) )
27 26 com13 
 |-  ( ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ f finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( x = ( f ( linC ` M ) V ) -> ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ x e. ( Base ` M ) ) -> x e. S ) ) )
28 27 impr 
 |-  ( ( f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) ) -> ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ x e. ( Base ` M ) ) -> x e. S ) )
29 28 rexlimiva 
 |-  ( E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) -> ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ x e. ( Base ` M ) ) -> x e. S ) )
30 29 com12 
 |-  ( ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) /\ x e. ( Base ` M ) ) -> ( E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) -> x e. S ) )
31 30 expimpd 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( ( x e. ( Base ` M ) /\ E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ x = ( f ( linC ` M ) V ) ) ) -> x e. S ) )
32 19 31 sylbid 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> ( x e. ( M LinCo V ) -> x e. S ) )
33 32 ralrimiv 
 |-  ( ( M e. LMod /\ S e. ( LSubSp ` M ) /\ V C_ S ) -> A. x e. ( M LinCo V ) x e. S )