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 ∅ = 0 M

Proof

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