Metamath Proof Explorer

Theorem lincvalsc0

Description: The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019)

Ref Expression
Hypotheses lincvalsc0.b ⊢ B = Base M
lincvalsc0.s ⊢ S = Scalar ⁡ M
lincvalsc0.0 ⊢ 0 ˙ = 0 S
lincvalsc0.z ⊢ Z = 0 M
lincvalsc0.f ⊢ F = x ∈ V ⟼ 0 ˙
Assertion lincvalsc0 ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = Z

Proof

Step Hyp Ref Expression
1 lincvalsc0.b ⊢ B = Base M
2 lincvalsc0.s ⊢ S = Scalar ⁡ M
3 lincvalsc0.0 ⊢ 0 ˙ = 0 S
4 lincvalsc0.z ⊢ Z = 0 M
5 lincvalsc0.f ⊢ F = x ∈ V ⟼ 0 ˙
6 simpl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → M ∈ LMod
7 2 eqcomi ⊢ Scalar ⁡ M = S
8 7 fveq2i ⊢ Base Scalar ⁡ M = Base S
9 2 8 3 lmod0cl ⊢ M ∈ LMod → 0 ˙ ∈ Base Scalar ⁡ M
10 9 adantr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → 0 ˙ ∈ Base Scalar ⁡ M
11 10 adantr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ x ∈ V → 0 ˙ ∈ Base Scalar ⁡ M
12 11 5 fmptd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F : V ⟶ Base Scalar ⁡ M
13 fvexd ⊢ M ∈ LMod → Base Scalar ⁡ M ∈ V
14 elmapg ⊢ Base Scalar ⁡ M ∈ V ∧ V ∈ 𝒫 B → F ∈ Base Scalar ⁡ M V ↔ F : V ⟶ Base Scalar ⁡ M
15 13 14 sylan ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F ∈ Base Scalar ⁡ M V ↔ F : V ⟶ Base Scalar ⁡ M
16 12 15 mpbird ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F ∈ Base Scalar ⁡ M V
17 1 pweqi ⊢ 𝒫 B = 𝒫 Base M
18 17 eleq2i ⊢ V ∈ 𝒫 B ↔ V ∈ 𝒫 Base M
19 18 bilani ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → V ∈ 𝒫 Base M
20 lincval ⊢ M ∈ LMod ∧ F ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → F linC ⁡ M V = ∑ M v ∈ V F ⁡ v ⋅ M v
21 6 16 19 20 syl3anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = ∑ M v ∈ V F ⁡ v ⋅ M v
22 simpr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → v ∈ V
23 3 fvexi ⊢ 0 ˙ ∈ V
24 eqidd ⊢ x = v → 0 ˙ = 0 ˙
25 24 5 fvmptg ⊢ v ∈ V ∧ 0 ˙ ∈ V → F ⁡ v = 0 ˙
26 22 23 25 sylancl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v = 0 ˙
27 26 oveq1d ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v ⋅ M v = 0 ˙ ⋅ M v
28 6 adantr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → M ∈ LMod
29 elelpwi ⊢ v ∈ V ∧ V ∈ 𝒫 B → v ∈ B
30 29 expcom ⊢ V ∈ 𝒫 B → v ∈ V → v ∈ B
31 30 adantl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → v ∈ V → v ∈ B
32 31 imp ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → v ∈ B
33 eqid ⊢ ⋅ M = ⋅ M
34 1 2 33 3 4 lmod0vs ⊢ M ∈ LMod ∧ v ∈ B → 0 ˙ ⋅ M v = Z
35 28 32 34 syl2anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → 0 ˙ ⋅ M v = Z
36 27 35 eqtrd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v ⋅ M v = Z
37 36 mpteq2dva ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → v ∈ V ⟼ F ⁡ v ⋅ M v = v ∈ V ⟼ Z
38 37 oveq2d ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → ∑ M v ∈ V F ⁡ v ⋅ M v = ∑ M v ∈ V Z
39 lmodgrp ⊢ M ∈ LMod → M ∈ Grp
40 39 grpmndd ⊢ M ∈ LMod → M ∈ Mnd
41 4 gsumz ⊢ M ∈ Mnd ∧ V ∈ 𝒫 B → ∑ M v ∈ V Z = Z
42 40 41 sylan ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → ∑ M v ∈ V Z = Z
43 21 38 42 3eqtrd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = Z