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. = ( 0g ` S )
lincvalsc0.z 
|- Z = ( 0g ` M )
lincvalsc0.f 
|- F = ( x e. V |-> .0. )
Assertion lincvalsc0 
|- ( ( M e. LMod /\ V e. ~P 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. = ( 0g ` S )
4 lincvalsc0.z 
 |-  Z = ( 0g ` M )
5 lincvalsc0.f 
 |-  F = ( x e. V |-> .0. )
6 simpl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> M e. LMod )
7 2 eqcomi 
 |-  ( Scalar ` M ) = S
8 7 fveq2i 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` S )
9 2 8 3 lmod0cl 
 |-  ( M e. LMod -> .0. e. ( Base ` ( Scalar ` M ) ) )
10 9 adantr 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> .0. e. ( Base ` ( Scalar ` M ) ) )
11 10 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. V ) -> .0. e. ( Base ` ( Scalar ` M ) ) )
12 11 5 fmptd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
13 fvexd 
 |-  ( M e. LMod -> ( Base ` ( Scalar ` M ) ) e. _V )
14 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P B ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
15 13 14 sylan 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
16 12 15 mpbird 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
17 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
18 17 eleq2i 
 |-  ( V e. ~P B <-> V e. ~P ( Base ` M ) )
19 18 biimpi 
 |-  ( V e. ~P B -> V e. ~P ( Base ` M ) )
20 19 adantl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> V e. ~P ( Base ` M ) )
21 lincval 
 |-  ( ( M e. LMod /\ F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
22 6 16 20 21 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
23 simpr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. V )
24 3 fvexi 
 |-  .0. e. _V
25 eqidd 
 |-  ( x = v -> .0. = .0. )
26 25 5 fvmptg 
 |-  ( ( v e. V /\ .0. e. _V ) -> ( F ` v ) = .0. )
27 23 24 26 sylancl 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( F ` v ) = .0. )
28 27 oveq1d 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = ( .0. ( .s ` M ) v ) )
29 6 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> M e. LMod )
30 elelpwi 
 |-  ( ( v e. V /\ V e. ~P B ) -> v e. B )
31 30 expcom 
 |-  ( V e. ~P B -> ( v e. V -> v e. B ) )
32 31 adantl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V -> v e. B ) )
33 32 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. B )
34 eqid 
 |-  ( .s ` M ) = ( .s ` M )
35 1 2 34 3 4 lmod0vs 
 |-  ( ( M e. LMod /\ v e. B ) -> ( .0. ( .s ` M ) v ) = Z )
36 29 33 35 syl2anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( .0. ( .s ` M ) v ) = Z )
37 28 36 eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = Z )
38 37 mpteq2dva 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) = ( v e. V |-> Z ) )
39 38 oveq2d 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) = ( M gsum ( v e. V |-> Z ) ) )
40 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
41 40 grpmndd 
 |-  ( M e. LMod -> M e. Mnd )
42 4 gsumz 
 |-  ( ( M e. Mnd /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
43 41 42 sylan 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
44 22 39 43 3eqtrd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )