Metamath Proof Explorer

Theorem lcoss

Description: A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion lcoss 
|- ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V C_ ( M LinCo V ) )

Proof

Step Hyp Ref Expression
1 elelpwi 
 |-  ( ( v e. V /\ V e. ~P ( Base ` M ) ) -> v e. ( Base ` M ) )
2 1 expcom 
 |-  ( V e. ~P ( Base ` M ) -> ( v e. V -> v e. ( Base ` M ) ) )
3 2 adantl 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. V -> v e. ( Base ` M ) ) )
4 3 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> v e. ( Base ` M ) )
5 eqid 
 |-  ( Base ` M ) = ( Base ` M )
6 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
7 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
8 eqid 
 |-  ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) )
9 equequ1 
 |-  ( x = y -> ( x = v <-> y = v ) )
10 9 ifbid 
 |-  ( x = y -> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) = if ( y = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
11 10 cbvmptv 
 |-  ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) = ( y e. V |-> if ( y = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
12 5 6 7 8 11 mptcfsupp 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ v e. V ) -> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
13 12 3expa 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
14 eqid 
 |-  ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) )
15 5 6 7 8 14 linc1 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) /\ v e. V ) -> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) = v )
16 15 3expa 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) = v )
17 16 eqcomd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> v = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) )
18 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
19 6 18 8 lmod1cl 
 |-  ( M e. LMod -> ( 1r ` ( Scalar ` M ) ) e. ( Base ` ( Scalar ` M ) ) )
20 6 18 7 lmod0cl 
 |-  ( M e. LMod -> ( 0g ` ( Scalar ` M ) ) e. ( Base ` ( Scalar ` M ) ) )
21 19 20 ifcld 
 |-  ( M e. LMod -> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
22 21 ad3antrrr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) /\ x e. V ) -> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) e. ( Base ` ( Scalar ` M ) ) )
23 22 fmpttd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) : V --> ( Base ` ( Scalar ` M ) ) )
24 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
25 simplr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> V e. ~P ( Base ` M ) )
26 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P ( Base ` M ) ) -> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) : V --> ( Base ` ( Scalar ` M ) ) ) )
27 24 25 26 sylancr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) : V --> ( Base ` ( Scalar ` M ) ) ) )
28 23 27 mpbird 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
29 breq1 
 |-  ( f = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( f finSupp ( 0g ` ( Scalar ` M ) ) <-> ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) ) )
30 oveq1 
 |-  ( f = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( f ( linC ` M ) V ) = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) )
31 30 eqeq2d 
 |-  ( f = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( v = ( f ( linC ` M ) V ) <-> v = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) ) )
32 29 31 anbi12d 
 |-  ( f = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) <-> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) ) ) )
33 32 adantl 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) /\ f = ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ) -> ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) <-> ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) ) ) )
34 28 33 rspcedv 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( ( x e. V |-> if ( x = v , ( 1r ` ( Scalar ` M ) ) , ( 0g ` ( Scalar ` M ) ) ) ) ( linC ` M ) V ) ) -> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) ) )
35 13 17 34 mp2and 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) )
36 5 6 18 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. ( M LinCo V ) <-> ( v e. ( Base ` M ) /\ E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) ) ) )
37 36 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> ( v e. ( M LinCo V ) <-> ( v e. ( Base ` M ) /\ E. f e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ v = ( f ( linC ` M ) V ) ) ) ) )
38 4 35 37 mpbir2and 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ v e. V ) -> v e. ( M LinCo V ) )
39 38 ex 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. V -> v e. ( M LinCo V ) ) )
40 39 ssrdv 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V C_ ( M LinCo V ) )