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 biimpi ⊢ V ∈ 𝒫 B → V ∈ 𝒫 Base M
20 19 adantl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → V ∈ 𝒫 Base M
21 lincval ⊢ M ∈ LMod ∧ F ∈ Base Scalar ⁡ M V ∧ V ∈ 𝒫 Base M → F linC ⁡ M V = ∑ M v ∈ V F ⁡ v ⋅ M v
22 6 16 20 21 syl3anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = ∑ M v ∈ V F ⁡ v ⋅ M v
23 simpr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → v ∈ V
24 3 fvexi ⊢ 0 ˙ ∈ V
25 eqidd ⊢ x = v → 0 ˙ = 0 ˙
26 25 5 fvmptg ⊢ v ∈ V ∧ 0 ˙ ∈ V → F ⁡ v = 0 ˙
27 23 24 26 sylancl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v = 0 ˙
28 27 oveq1d ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v ⋅ M v = 0 ˙ ⋅ M v
29 6 adantr ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → M ∈ LMod
30 elelpwi ⊢ v ∈ V ∧ V ∈ 𝒫 B → v ∈ B
31 30 expcom ⊢ V ∈ 𝒫 B → v ∈ V → v ∈ B
32 31 adantl ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → v ∈ V → v ∈ B
33 32 imp ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → v ∈ B
34 eqid ⊢ ⋅ M = ⋅ M
35 1 2 34 3 4 lmod0vs ⊢ M ∈ LMod ∧ v ∈ B → 0 ˙ ⋅ M v = Z
36 29 33 35 syl2anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → 0 ˙ ⋅ M v = Z
37 28 36 eqtrd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B ∧ v ∈ V → F ⁡ v ⋅ M v = Z
38 37 mpteq2dva ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → v ∈ V ⟼ F ⁡ v ⋅ M v = v ∈ V ⟼ Z
39 38 oveq2d ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → ∑ M v ∈ V F ⁡ v ⋅ M v = ∑ M v ∈ V Z
40 lmodgrp ⊢ M ∈ LMod → M ∈ Grp
41 grpmnd ⊢ M ∈ Grp → M ∈ Mnd
42 40 41 syl ⊢ M ∈ LMod → M ∈ Mnd
43 4 gsumz ⊢ M ∈ Mnd ∧ V ∈ 𝒫 B → ∑ M v ∈ V Z = Z
44 42 43 sylan ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → ∑ M v ∈ V Z = Z
45 22 39 44 3eqtrd ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = Z