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 syl5ibr
 |-  ( 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 )