Metamath Proof Explorer

Theorem lincfsuppcl

Description: A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincfsuppcl.b 
|- B = ( Base ` M )
lincfsuppcl.r 
|- R = ( Scalar ` M )
lincfsuppcl.s 
|- S = ( Base ` R )
lincfsuppcl.0 
|- .0. = ( 0g ` R )
Assertion lincfsuppcl 
|- ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( F ( linC ` M ) V ) e. B )

Proof

Step Hyp Ref Expression
1 lincfsuppcl.b 
 |-  B = ( Base ` M )
2 lincfsuppcl.r 
 |-  R = ( Scalar ` M )
3 lincfsuppcl.s 
 |-  S = ( Base ` R )
4 lincfsuppcl.0 
 |-  .0. = ( 0g ` R )
5 simp1 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> M e. LMod )
6 2 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
7 3 6 eqtri 
 |-  S = ( Base ` ( Scalar ` M ) )
8 7 oveq1i 
 |-  ( S ^m V ) = ( ( Base ` ( Scalar ` M ) ) ^m V )
9 8 eleq2i 
 |-  ( F e. ( S ^m V ) <-> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
10 9 birani 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
11 10 3ad2ant3 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
12 elpwg 
 |-  ( V e. W -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
13 1 a1i 
 |-  ( V e. W -> B = ( Base ` M ) )
14 13 eqcomd 
 |-  ( V e. W -> ( Base ` M ) = B )
15 14 sseq2d 
 |-  ( V e. W -> ( V C_ ( Base ` M ) <-> V C_ B ) )
16 12 15 bitr2d 
 |-  ( V e. W -> ( V C_ B <-> V e. ~P ( Base ` M ) ) )
17 16 biimpa 
 |-  ( ( V e. W /\ V C_ B ) -> V e. ~P ( Base ` M ) )
18 17 3ad2ant2 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> V e. ~P ( Base ` M ) )
19 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 ) ) ) )
20 5 11 18 19 syl3anc 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
21 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
22 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
23 22 3ad2ant1 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> M e. CMnd )
24 simpl 
 |-  ( ( V e. W /\ V C_ B ) -> V e. W )
25 24 3ad2ant2 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> V e. W )
26 5 adantr 
 |-  ( ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ v e. V ) -> M e. LMod )
27 elmapi 
 |-  ( F e. ( S ^m V ) -> F : V --> S )
28 ffvelcdm 
 |-  ( ( F : V --> S /\ v e. V ) -> ( F ` v ) e. S )
29 28 ex 
 |-  ( F : V --> S -> ( v e. V -> ( F ` v ) e. S ) )
30 27 29 syl 
 |-  ( F e. ( S ^m V ) -> ( v e. V -> ( F ` v ) e. S ) )
31 30 adantr 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> ( v e. V -> ( F ` v ) e. S ) )
32 31 3ad2ant3 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( v e. V -> ( F ` v ) e. S ) )
33 32 imp 
 |-  ( ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ v e. V ) -> ( F ` v ) e. S )
34 ssel 
 |-  ( V C_ B -> ( v e. V -> v e. B ) )
35 34 adantl 
 |-  ( ( V e. W /\ V C_ B ) -> ( v e. V -> v e. B ) )
36 35 3ad2ant2 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( v e. V -> v e. B ) )
37 36 imp 
 |-  ( ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ v e. V ) -> v e. B )
38 eqid 
 |-  ( .s ` M ) = ( .s ` M )
39 1 2 38 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` v ) e. S /\ v e. B ) -> ( ( F ` v ) ( .s ` M ) v ) e. B )
40 26 33 37 39 syl3anc 
 |-  ( ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) e. B )
41 40 fmpttd 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) : V --> B )
42 simpl 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> F e. ( S ^m V ) )
43 42 3ad2ant3 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> F e. ( S ^m V ) )
44 simp3r 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> F finSupp .0. )
45 44 4 breqtrdi 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> F finSupp ( 0g ` R ) )
46 2 3 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ F e. ( S ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
47 5 18 43 45 46 syl211anc 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
48 1 21 23 25 41 47 gsumcl 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) e. B )
49 20 48 eqeltrd 
 |-  ( ( M e. LMod /\ ( V e. W /\ V C_ B ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( F ( linC ` M ) V ) e. B )