Metamath Proof Explorer

Theorem lincscm

Description: A linear combinations multiplied with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 9-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincscm.s 
|- .xb = ( .s ` M )
lincscm.t 
|- .x. = ( .r ` ( Scalar ` M ) )
lincscm.x 
|- X = ( A ( linC ` M ) V )
lincscm.r 
|- R = ( Base ` ( Scalar ` M ) )
lincscm.f 
|- F = ( x e. V |-> ( S .x. ( A ` x ) ) )
Assertion lincscm 
|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( S .xb X ) = ( F ( linC ` M ) V ) )

Proof

Step Hyp Ref Expression
1 lincscm.s 
 |-  .xb = ( .s ` M )
2 lincscm.t 
 |-  .x. = ( .r ` ( Scalar ` M ) )
3 lincscm.x 
 |-  X = ( A ( linC ` M ) V )
4 lincscm.r 
 |-  R = ( Base ` ( Scalar ` M ) )
5 lincscm.f 
 |-  F = ( x e. V |-> ( S .x. ( A ` x ) ) )
6 eqid 
 |-  ( Base ` M ) = ( Base ` M )
7 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
8 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
9 eqid 
 |-  ( +g ` M ) = ( +g ` M )
10 simp1l 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> M e. LMod )
11 simpr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
12 11 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> V e. ~P ( Base ` M ) )
13 simpr 
 |-  ( ( A e. ( R ^m V ) /\ S e. R ) -> S e. R )
14 13 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> S e. R )
15 10 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> M e. LMod )
16 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
17 ffvelcdm 
 |-  ( ( A : V --> R /\ v e. V ) -> ( A ` v ) e. R )
18 17 ex 
 |-  ( A : V --> R -> ( v e. V -> ( A ` v ) e. R ) )
19 16 18 syl 
 |-  ( A e. ( R ^m V ) -> ( v e. V -> ( A ` v ) e. R ) )
20 19 adantr 
 |-  ( ( A e. ( R ^m V ) /\ S e. R ) -> ( v e. V -> ( A ` v ) e. R ) )
21 20 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V -> ( A ` v ) e. R ) )
22 21 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( A ` v ) e. R )
23 elelpwi 
 |-  ( ( v e. V /\ V e. ~P ( Base ` M ) ) -> v e. ( Base ` M ) )
24 23 expcom 
 |-  ( V e. ~P ( Base ` M ) -> ( v e. V -> v e. ( Base ` M ) ) )
25 24 adantl 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( v e. V -> v e. ( Base ` M ) ) )
26 25 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V -> v e. ( Base ` M ) ) )
27 26 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> v e. ( Base ` M ) )
28 eqid 
 |-  ( .s ` M ) = ( .s ` M )
29 6 7 28 4 lmodvscl 
 |-  ( ( M e. LMod /\ ( A ` v ) e. R /\ v e. ( Base ` M ) ) -> ( ( A ` v ) ( .s ` M ) v ) e. ( Base ` M ) )
30 15 22 27 29 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( ( A ` v ) ( .s ` M ) v ) e. ( Base ` M ) )
31 7 4 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
32 31 3adant2r 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) finSupp ( 0g ` M ) )
33 6 7 4 8 9 1 10 12 14 30 32 gsumvsmul 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( M gsum ( v e. V |-> ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) ) ) = ( S .xb ( M gsum ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ) ) )
34 7 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
35 34 adantr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( Scalar ` M ) e. Ring )
36 35 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( Scalar ` M ) e. Ring )
37 36 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ x e. V ) -> ( Scalar ` M ) e. Ring )
38 4 eleq2i 
 |-  ( S e. R <-> S e. ( Base ` ( Scalar ` M ) ) )
39 38 biimpi 
 |-  ( S e. R -> S e. ( Base ` ( Scalar ` M ) ) )
40 39 adantl 
 |-  ( ( A e. ( R ^m V ) /\ S e. R ) -> S e. ( Base ` ( Scalar ` M ) ) )
41 40 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> S e. ( Base ` ( Scalar ` M ) ) )
42 41 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ x e. V ) -> S e. ( Base ` ( Scalar ` M ) ) )
43 ffvelcdm 
 |-  ( ( A : V --> R /\ x e. V ) -> ( A ` x ) e. R )
44 43 4 eleqtrdi 
 |-  ( ( A : V --> R /\ x e. V ) -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) )
45 44 ex 
 |-  ( A : V --> R -> ( x e. V -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) ) )
46 16 45 syl 
 |-  ( A e. ( R ^m V ) -> ( x e. V -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) ) )
47 46 adantr 
 |-  ( ( A e. ( R ^m V ) /\ S e. R ) -> ( x e. V -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) ) )
48 47 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( x e. V -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) ) )
49 48 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ x e. V ) -> ( A ` x ) e. ( Base ` ( Scalar ` M ) ) )
50 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
51 50 2 ringcl 
 |-  ( ( ( Scalar ` M ) e. Ring /\ S e. ( Base ` ( Scalar ` M ) ) /\ ( A ` x ) e. ( Base ` ( Scalar ` M ) ) ) -> ( S .x. ( A ` x ) ) e. ( Base ` ( Scalar ` M ) ) )
52 37 42 49 51 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ x e. V ) -> ( S .x. ( A ` x ) ) e. ( Base ` ( Scalar ` M ) ) )
53 52 5 fmptd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
54 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
55 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P ( Base ` M ) ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
56 54 12 55 sylancr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
57 53 56 mpbird 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
58 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 ) ) ) )
59 10 57 12 58 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
60 simpr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> v e. V )
61 ovex 
 |-  ( S .x. ( A ` v ) ) e. _V
62 fveq2 
 |-  ( x = v -> ( A ` x ) = ( A ` v ) )
63 62 oveq2d 
 |-  ( x = v -> ( S .x. ( A ` x ) ) = ( S .x. ( A ` v ) ) )
64 63 5 fvmptg 
 |-  ( ( v e. V /\ ( S .x. ( A ` v ) ) e. _V ) -> ( F ` v ) = ( S .x. ( A ` v ) ) )
65 60 61 64 sylancl 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( F ` v ) = ( S .x. ( A ` v ) ) )
66 65 oveq1d 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = ( ( S .x. ( A ` v ) ) ( .s ` M ) v ) )
67 14 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> S e. R )
68 6 7 28 4 2 lmodvsass 
 |-  ( ( M e. LMod /\ ( S e. R /\ ( A ` v ) e. R /\ v e. ( Base ` M ) ) ) -> ( ( S .x. ( A ` v ) ) ( .s ` M ) v ) = ( S ( .s ` M ) ( ( A ` v ) ( .s ` M ) v ) ) )
69 15 67 22 27 68 syl13anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( ( S .x. ( A ` v ) ) ( .s ` M ) v ) = ( S ( .s ` M ) ( ( A ` v ) ( .s ` M ) v ) ) )
70 1 eqcomi 
 |-  ( .s ` M ) = .xb
71 70 a1i 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( .s ` M ) = .xb )
72 71 oveqd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( S ( .s ` M ) ( ( A ` v ) ( .s ` M ) v ) ) = ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) )
73 69 72 eqtrd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( ( S .x. ( A ` v ) ) ( .s ` M ) v ) = ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) )
74 66 73 eqtrd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) )
75 74 mpteq2dva 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) = ( v e. V |-> ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) ) )
76 75 oveq2d 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) = ( M gsum ( v e. V |-> ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) ) ) )
77 59 76 eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( S .xb ( ( A ` v ) ( .s ` M ) v ) ) ) ) )
78 3 a1i 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> X = ( A ( linC ` M ) V ) )
79 4 oveq1i 
 |-  ( R ^m V ) = ( ( Base ` ( Scalar ` M ) ) ^m V )
80 79 eleq2i 
 |-  ( A e. ( R ^m V ) <-> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
81 80 biimpi 
 |-  ( A e. ( R ^m V ) -> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
82 81 adantr 
 |-  ( ( A e. ( R ^m V ) /\ S e. R ) -> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
83 82 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
84 lincval 
 |-  ( ( M e. LMod /\ A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( A ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ) )
85 10 83 12 84 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( A ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ) )
86 78 85 eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> X = ( M gsum ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ) )
87 86 oveq2d 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( S .xb X ) = ( S .xb ( M gsum ( v e. V |-> ( ( A ` v ) ( .s ` M ) v ) ) ) ) )
88 33 77 87 3eqtr4rd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ S e. R ) /\ A finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( S .xb X ) = ( F ( linC ` M ) V ) )