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