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∈LMod∧V∈𝒫BaseM→0M∈MLinCoV

Proof

Step Hyp Ref Expression
1 fvex ⊢0M∈V
2 1 snid ⊢0M∈0M
3 oveq2 ⊢V=∅→MLinCoV=MLinCo∅
4 lmodgrp ⊢M∈LMod→M∈Grp
5 grpmnd ⊢M∈Grp→M∈Mnd
6 lco0 ⊢M∈Mnd→MLinCo∅=0M
7 4 5 6 3syl ⊢M∈LMod→MLinCo∅=0M
8 7 adantr ⊢M∈LMod∧V∈𝒫BaseM→MLinCo∅=0M
9 3 8 sylan9eq ⊢V=∅∧M∈LMod∧V∈𝒫BaseM→MLinCoV=0M
10 2 9 eleqtrrid ⊢V=∅∧M∈LMod∧V∈𝒫BaseM→0M∈MLinCoV
11 eqid ⊢BaseM=BaseM
12 eqid ⊢0M=0M
13 11 12 lmod0vcl ⊢M∈LMod→0M∈BaseM
14 13 adantr ⊢M∈LMod∧V∈𝒫BaseM→0M∈BaseM
15 14 adantl ⊢¬V=∅∧M∈LMod∧V∈𝒫BaseM→0M∈BaseM
16 eqid ⊢Scalar⁡M=Scalar⁡M
17 eqid ⊢0Scalar⁡M=0Scalar⁡M
18 eqidd ⊢v=w→0Scalar⁡M=0Scalar⁡M
19 18 cbvmptv ⊢v∈V⟼0Scalar⁡M=w∈V⟼0Scalar⁡M
20 eqid ⊢BaseScalar⁡M=BaseScalar⁡M
21 11 16 17 12 19 20 lcoc0 ⊢M∈LMod∧V∈𝒫BaseM→v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M
22 21 adantl ⊢¬V=∅∧M∈LMod∧V∈𝒫BaseM→v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M
23 simpl ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧¬V=∅∧M∈LMod∧V∈𝒫BaseM→v∈V⟼0Scalar⁡M∈BaseScalar⁡MV
24 breq1 ⊢s=v∈V⟼0Scalar⁡M→finSupp0Scalar⁡M⁡s↔finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M
25 oveq1 ⊢s=v∈V⟼0Scalar⁡M→slinC⁡MV=v∈V⟼0Scalar⁡MlinC⁡MV
26 25 eqeq2d ⊢s=v∈V⟼0Scalar⁡M→0M=slinC⁡MV↔0M=v∈V⟼0Scalar⁡MlinC⁡MV
27 eqcom ⊢0M=v∈V⟼0Scalar⁡MlinC⁡MV↔v∈V⟼0Scalar⁡MlinC⁡MV=0M
28 26 27 bitrdi ⊢s=v∈V⟼0Scalar⁡M→0M=slinC⁡MV↔v∈V⟼0Scalar⁡MlinC⁡MV=0M
29 24 28 anbi12d ⊢s=v∈V⟼0Scalar⁡M→finSupp0Scalar⁡M⁡s∧0M=slinC⁡MV↔finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M
30 29 adantl ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧¬V=∅∧M∈LMod∧V∈𝒫BaseM∧s=v∈V⟼0Scalar⁡M→finSupp0Scalar⁡M⁡s∧0M=slinC⁡MV↔finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M
31 23 30 rspcedv ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧¬V=∅∧M∈LMod∧V∈𝒫BaseM→finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M→∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
32 31 ex ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV→¬V=∅∧M∈LMod∧V∈𝒫BaseM→finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M→∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
33 32 com23 ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV→finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M→¬V=∅∧M∈LMod∧V∈𝒫BaseM→∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
34 33 3impib ⊢v∈V⟼0Scalar⁡M∈BaseScalar⁡MV∧finSupp0Scalar⁡M⁡v∈V⟼0Scalar⁡M∧v∈V⟼0Scalar⁡MlinC⁡MV=0M→¬V=∅∧M∈LMod∧V∈𝒫BaseM→∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
35 22 34 mpcom ⊢¬V=∅∧M∈LMod∧V∈𝒫BaseM→∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
36 11 16 20 lcoval ⊢M∈LMod∧V∈𝒫BaseM→0M∈MLinCoV↔0M∈BaseM∧∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
37 36 adantl ⊢¬V=∅∧M∈LMod∧V∈𝒫BaseM→0M∈MLinCoV↔0M∈BaseM∧∃s∈BaseScalar⁡MVfinSupp0Scalar⁡M⁡s∧0M=slinC⁡MV
38 15 35 37 mpbir2and ⊢¬V=∅∧M∈LMod∧V∈𝒫BaseM→0M∈MLinCoV
39 10 38 pm2.61ian ⊢M∈LMod∧V∈𝒫BaseM→0M∈MLinCoV