Metamath Proof Explorer

Theorem linccl

Description: A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019)

Ref Expression
Hypotheses linccl.b 
|- B = ( Base ` M )
linccl.r 
|- R = ( Base ` ( Scalar ` M ) )
Assertion linccl 
|- ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( S ( linC ` M ) V ) e. B )

Proof

Step Hyp Ref Expression
1 linccl.b 
 |-  B = ( Base ` M )
2 linccl.r 
 |-  R = ( Base ` ( Scalar ` M ) )
3 simpl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> M e. LMod )
4 2 oveq1i 
 |-  ( R ^m V ) = ( ( Base ` ( Scalar ` M ) ) ^m V )
5 4 eleq2i 
 |-  ( S e. ( R ^m V ) <-> S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
6 5 biimpi 
 |-  ( S e. ( R ^m V ) -> S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
7 6 3ad2ant3 
 |-  ( ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) -> S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
8 7 adantl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
9 1 sseq2i 
 |-  ( V C_ B <-> V C_ ( Base ` M ) )
10 fvex 
 |-  ( Base ` M ) e. _V
11 10 ssex 
 |-  ( V C_ ( Base ` M ) -> V e. _V )
12 elpwg 
 |-  ( V e. _V -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
13 11 12 syl 
 |-  ( V C_ ( Base ` M ) -> ( V e. ~P ( Base ` M ) <-> V C_ ( Base ` M ) ) )
14 13 ibir 
 |-  ( V C_ ( Base ` M ) -> V e. ~P ( Base ` M ) )
15 9 14 sylbi 
 |-  ( V C_ B -> V e. ~P ( Base ` M ) )
16 15 3ad2ant2 
 |-  ( ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) -> V e. ~P ( Base ` M ) )
17 16 adantl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> V e. ~P ( Base ` M ) )
18 lincval 
 |-  ( ( M e. LMod /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) ) )
19 3 8 17 18 syl3anc 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( S ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) ) )
20 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
21 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
22 21 adantr 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> M e. CMnd )
23 simpr1 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> V e. Fin )
24 3 adantr 
 |-  ( ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) /\ v e. V ) -> M e. LMod )
25 2 fvexi 
 |-  R e. _V
26 elmapg 
 |-  ( ( R e. _V /\ V e. Fin ) -> ( S e. ( R ^m V ) <-> S : V --> R ) )
27 25 26 mpan 
 |-  ( V e. Fin -> ( S e. ( R ^m V ) <-> S : V --> R ) )
28 ffvelcdm 
 |-  ( ( S : V --> R /\ v e. V ) -> ( S ` v ) e. R )
29 28 ex 
 |-  ( S : V --> R -> ( v e. V -> ( S ` v ) e. R ) )
30 27 29 biimtrdi 
 |-  ( V e. Fin -> ( S e. ( R ^m V ) -> ( v e. V -> ( S ` v ) e. R ) ) )
31 30 imp 
 |-  ( ( V e. Fin /\ S e. ( R ^m V ) ) -> ( v e. V -> ( S ` v ) e. R ) )
32 31 3adant2 
 |-  ( ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) -> ( v e. V -> ( S ` v ) e. R ) )
33 32 adantl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( v e. V -> ( S ` v ) e. R ) )
34 33 imp 
 |-  ( ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) /\ v e. V ) -> ( S ` v ) e. R )
35 ssel 
 |-  ( V C_ B -> ( v e. V -> v e. B ) )
36 35 3ad2ant2 
 |-  ( ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) -> ( v e. V -> v e. B ) )
37 36 adantl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( v e. V -> v e. B ) )
38 37 imp 
 |-  ( ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) /\ v e. V ) -> v e. B )
39 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
40 eqid 
 |-  ( .s ` M ) = ( .s ` M )
41 1 39 40 2 lmodvscl 
 |-  ( ( M e. LMod /\ ( S ` v ) e. R /\ v e. B ) -> ( ( S ` v ) ( .s ` M ) v ) e. B )
42 24 34 38 41 syl3anc 
 |-  ( ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( S ` v ) ( .s ` M ) v ) e. B )
43 42 fmpttd 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) : V --> B )
44 16 anim2i 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
45 simpr3 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> S e. ( R ^m V ) )
46 elmapi 
 |-  ( S e. ( R ^m V ) -> S : V --> R )
47 46 3ad2ant3 
 |-  ( ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) -> S : V --> R )
48 47 adantl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> S : V --> R )
49 fvexd 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( 0g ` ( Scalar ` M ) ) e. _V )
50 48 23 49 fdmfifsupp 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> S finSupp ( 0g ` ( Scalar ` M ) ) )
51 39 2 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ S e. ( R ^m V ) /\ S finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
52 44 45 50 51 syl3anc 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
53 1 20 22 23 43 52 gsumcl 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( M gsum ( v e. V |-> ( ( S ` v ) ( .s ` M ) v ) ) ) e. B )
54 19 53 eqeltrd 
 |-  ( ( M e. LMod /\ ( V e. Fin /\ V C_ B /\ S e. ( R ^m V ) ) ) -> ( S ( linC ` M ) V ) e. B )