Metamath Proof Explorer

Theorem lcoc0

Description: Properties of a linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019) (Revised by AV, 28-Jul-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. )
lcoc0.r 
|- R = ( Base ` S )
Assertion lcoc0 
|- ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( R ^m V ) /\ F finSupp .0. /\ ( 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 lcoc0.r 
 |-  R = ( Base ` S )
7 2 6 3 lmod0cl 
 |-  ( M e. LMod -> .0. e. R )
8 7 ad2antrr 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. V ) -> .0. e. R )
9 8 5 fmptd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> F : V --> R )
10 6 fvexi 
 |-  R e. _V
11 10 a1i 
 |-  ( M e. LMod -> R e. _V )
12 elmapg 
 |-  ( ( R e. _V /\ V e. ~P B ) -> ( F e. ( R ^m V ) <-> F : V --> R ) )
13 11 12 sylan 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( R ^m V ) <-> F : V --> R ) )
14 9 13 mpbird 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> F e. ( R ^m V ) )
15 eqidd 
 |-  ( x = v -> .0. = .0. )
16 15 cbvmptv 
 |-  ( x e. V |-> .0. ) = ( v e. V |-> .0. )
17 5 16 eqtri 
 |-  F = ( v e. V |-> .0. )
18 simpr 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> V e. ~P B )
19 3 fvexi 
 |-  .0. e. _V
20 19 a1i 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> .0. e. _V )
21 19 a1i 
 |-  ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> .0. e. _V )
22 17 18 20 21 mptsuppd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F supp .0. ) = { v e. V | .0. =/= .0. } )
23 neirr 
 |-  -. .0. =/= .0.
24 23 a1i 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> -. .0. =/= .0. )
25 24 ralrimivw 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> A. v e. V -. .0. =/= .0. )
26 rabeq0 
 |-  ( { v e. V | .0. =/= .0. } = (/) <-> A. v e. V -. .0. =/= .0. )
27 25 26 sylibr 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> { v e. V | .0. =/= .0. } = (/) )
28 0fin 
 |-  (/) e. Fin
29 28 a1i 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> (/) e. Fin )
30 27 29 eqeltrd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> { v e. V | .0. =/= .0. } e. Fin )
31 22 30 eqeltrd 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F supp .0. ) e. Fin )
32 5 funmpt2 
 |-  Fun F
33 32 a1i 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> Fun F )
34 funisfsupp 
 |-  ( ( Fun F /\ F e. ( R ^m V ) /\ .0. e. _V ) -> ( F finSupp .0. <-> ( F supp .0. ) e. Fin ) )
35 33 14 20 34 syl3anc 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F finSupp .0. <-> ( F supp .0. ) e. Fin ) )
36 31 35 mpbird 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> F finSupp .0. )
37 1 2 3 4 5 lincvalsc0 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )
38 14 36 37 3jca 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( R ^m V ) /\ F finSupp .0. /\ ( F ( linC ` M ) V ) = Z ) )