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 40 grpmndd M LMod M Mnd
42 4 gsumz M Mnd V 𝒫 B M v V Z = Z
43 41 42 sylan M LMod V 𝒫 B M v V Z = Z
44 22 39 43 3eqtrd M LMod V 𝒫 B F linC M V = Z