Metamath Proof Explorer

Theorem lincval0

Description: The value of an empty linear combination. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lincval0 ⊢M∈X→∅linC⁡M∅=0M

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 1 snid ⊢∅∈∅
3 fvex ⊢BaseScalar⁡M∈V
4 map0e ⊢BaseScalar⁡M∈V→BaseScalar⁡M∅=1𝑜
5 3 4 mp1i ⊢M∈X→BaseScalar⁡M∅=1𝑜
6 df1o2 ⊢1𝑜=∅
7 5 6 eqtrdi ⊢M∈X→BaseScalar⁡M∅=∅
8 2 7 eleqtrrid ⊢M∈X→∅∈BaseScalar⁡M∅
9 0elpw ⊢∅∈𝒫BaseM
10 9 a1i ⊢M∈X→∅∈𝒫BaseM
11 lincval ⊢M∈X∧∅∈BaseScalar⁡M∅∧∅∈𝒫BaseM→∅linC⁡M∅=∑Mv∈∅∅⁡v⋅Mv
12 8 10 11 mpd3an23 ⊢M∈X→∅linC⁡M∅=∑Mv∈∅∅⁡v⋅Mv
13 mpt0 ⊢v∈∅⟼∅⁡v⋅Mv=∅
14 13 a1i ⊢M∈X→v∈∅⟼∅⁡v⋅Mv=∅
15 14 oveq2d ⊢M∈X→∑Mv∈∅∅⁡v⋅Mv=∑M∅
16 eqid ⊢0M=0M
17 16 gsum0 ⊢∑M∅=0M
18 15 17 eqtrdi ⊢M∈X→∑Mv∈∅∅⁡v⋅Mv=0M
19 12 18 eqtrd ⊢M∈X→∅linC⁡M∅=0M