Metamath Proof Explorer

Theorem lcoel0

Description: The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( 0g ` M ) e. _V
2 1 snid 
 |-  ( 0g ` M ) e. { ( 0g ` M ) }
3 oveq2 
 |-  ( V = (/) -> ( M LinCo V ) = ( M LinCo (/) ) )
4 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
5 grpmnd 
 |-  ( M e. Grp -> M e. Mnd )
6 lco0 
 |-  ( M e. Mnd -> ( M LinCo (/) ) = { ( 0g ` M ) } )
7 4 5 6 3syl 
 |-  ( M e. LMod -> ( M LinCo (/) ) = { ( 0g ` M ) } )
8 7 adantr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M LinCo (/) ) = { ( 0g ` M ) } )
9 3 8 sylan9eq 
 |-  ( ( V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( M LinCo V ) = { ( 0g ` M ) } )
10 2 9 eleqtrrid 
 |-  ( ( V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( 0g ` M ) e. ( M LinCo V ) )
11 eqid 
 |-  ( Base ` M ) = ( Base ` M )
12 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
13 11 12 lmod0vcl 
 |-  ( M e. LMod -> ( 0g ` M ) e. ( Base ` M ) )
14 13 adantr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( 0g ` M ) e. ( Base ` M ) )
15 14 adantl 
 |-  ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( 0g ` M ) e. ( Base ` M ) )
16 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
17 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
18 eqidd 
 |-  ( v = w -> ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) ) )
19 18 cbvmptv 
 |-  ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) = ( w e. V |-> ( 0g ` ( Scalar ` M ) ) )
20 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
21 11 16 17 12 19 20 lcoc0 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) )
22 21 adantl 
 |-  ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) )
23 simpl 
 |-  ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) ) -> ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
24 breq1 
 |-  ( s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) -> ( s finSupp ( 0g ` ( Scalar ` M ) ) <-> ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) ) )
25 oveq1 
 |-  ( s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) -> ( s ( linC ` M ) V ) = ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) )
26 25 eqeq2d 
 |-  ( s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) -> ( ( 0g ` M ) = ( s ( linC ` M ) V ) <-> ( 0g ` M ) = ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) ) )
27 eqcom 
 |-  ( ( 0g ` M ) = ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) <-> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) )
28 26 27 bitrdi 
 |-  ( s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) -> ( ( 0g ` M ) = ( s ( linC ` M ) V ) <-> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) )
29 24 28 anbi12d 
 |-  ( s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) -> ( ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) <-> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) ) )
30 29 adantl 
 |-  ( ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) ) /\ s = ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) <-> ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) ) )
31 23 30 rspcedv 
 |-  ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) ) -> ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) )
32 31 ex 
 |-  ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) -> ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) ) )
33 32 com23 
 |-  ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) -> ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) -> ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) ) )
34 33 3impib 
 |-  ( ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( ( v e. V |-> ( 0g ` ( Scalar ` M ) ) ) ( linC ` M ) V ) = ( 0g ` M ) ) -> ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) )
35 22 34 mpcom 
 |-  ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) )
36 11 16 20 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( 0g ` M ) e. ( M LinCo V ) <-> ( ( 0g ` M ) e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) ) )
37 36 adantl 
 |-  ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( ( 0g ` M ) e. ( M LinCo V ) <-> ( ( 0g ` M ) e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( 0g ` M ) = ( s ( linC ` M ) V ) ) ) ) )
38 15 35 37 mpbir2and 
 |-  ( ( -. V = (/) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( 0g ` M ) e. ( M LinCo V ) )
39 10 38 pm2.61ian 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( 0g ` M ) e. ( M LinCo V ) )