Metamath Proof Explorer

Theorem lincsum

Description: The sum of two linear combinations is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 4-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincsum.p 
|- .+ = ( +g ` M )
lincsum.x 
|- X = ( A ( linC ` M ) V )
lincsum.y 
|- Y = ( B ( linC ` M ) V )
lincsum.s 
|- S = ( Scalar ` M )
lincsum.r 
|- R = ( Base ` S )
lincsum.b 
|- .+b = ( +g ` S )
Assertion lincsum 
|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( X .+ Y ) = ( ( A oF .+b B ) ( linC ` M ) V ) )

Proof

Step Hyp Ref Expression
1 lincsum.p 
 |-  .+ = ( +g ` M )
2 lincsum.x 
 |-  X = ( A ( linC ` M ) V )
3 lincsum.y 
 |-  Y = ( B ( linC ` M ) V )
4 lincsum.s 
 |-  S = ( Scalar ` M )
5 lincsum.r 
 |-  R = ( Base ` S )
6 lincsum.b 
 |-  .+b = ( +g ` S )
7 eqid 
 |-  ( Base ` M ) = ( Base ` M )
8 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
9 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
10 9 adantr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> M e. CMnd )
11 10 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> M e. CMnd )
12 simpr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
13 12 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> V e. ~P ( Base ` M ) )
14 simpl 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> M e. LMod )
15 14 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> M e. LMod )
16 15 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> M e. LMod )
17 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
18 ffvelrn 
 |-  ( ( A : V --> R /\ x e. V ) -> ( A ` x ) e. R )
19 18 ex 
 |-  ( A : V --> R -> ( x e. V -> ( A ` x ) e. R ) )
20 17 19 syl 
 |-  ( A e. ( R ^m V ) -> ( x e. V -> ( A ` x ) e. R ) )
21 20 adantr 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> ( x e. V -> ( A ` x ) e. R ) )
22 21 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V -> ( A ` x ) e. R ) )
23 22 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> ( A ` x ) e. R )
24 elelpwi 
 |-  ( ( x e. V /\ V e. ~P ( Base ` M ) ) -> x e. ( Base ` M ) )
25 24 expcom 
 |-  ( V e. ~P ( Base ` M ) -> ( x e. V -> x e. ( Base ` M ) ) )
26 25 adantl 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( x e. V -> x e. ( Base ` M ) ) )
27 26 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V -> x e. ( Base ` M ) ) )
28 27 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> x e. ( Base ` M ) )
29 eqid 
 |-  ( .s ` M ) = ( .s ` M )
30 7 4 29 5 lmodvscl 
 |-  ( ( M e. LMod /\ ( A ` x ) e. R /\ x e. ( Base ` M ) ) -> ( ( A ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
31 16 23 28 30 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> ( ( A ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
32 elmapi 
 |-  ( B e. ( R ^m V ) -> B : V --> R )
33 ffvelrn 
 |-  ( ( B : V --> R /\ x e. V ) -> ( B ` x ) e. R )
34 33 ex 
 |-  ( B : V --> R -> ( x e. V -> ( B ` x ) e. R ) )
35 32 34 syl 
 |-  ( B e. ( R ^m V ) -> ( x e. V -> ( B ` x ) e. R ) )
36 35 adantl 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> ( x e. V -> ( B ` x ) e. R ) )
37 36 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V -> ( B ` x ) e. R ) )
38 37 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> ( B ` x ) e. R )
39 7 4 29 5 lmodvscl 
 |-  ( ( M e. LMod /\ ( B ` x ) e. R /\ x e. ( Base ` M ) ) -> ( ( B ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
40 16 38 28 39 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) /\ x e. V ) -> ( ( B ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
41 eqidd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) = ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) )
42 eqidd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) = ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) )
43 id 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
44 simpl 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> A e. ( R ^m V ) )
45 simpl 
 |-  ( ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) -> A finSupp ( 0g ` S ) )
46 4 5 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ A e. ( R ^m V ) /\ A finSupp ( 0g ` S ) ) -> ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
47 43 44 45 46 syl3an 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
48 simpr 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> B e. ( R ^m V ) )
49 simpr 
 |-  ( ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) -> B finSupp ( 0g ` S ) )
50 4 5 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ B e. ( R ^m V ) /\ B finSupp ( 0g ` S ) ) -> ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
51 43 48 49 50 syl3an 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
52 7 8 1 11 13 31 40 41 42 47 51 gsummptfsadd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( M gsum ( x e. V |-> ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) ) ) = ( ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) .+ ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
53 12 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> V e. ~P ( Base ` M ) )
54 elmapfn 
 |-  ( A e. ( R ^m V ) -> A Fn V )
55 54 ad2antrl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> A Fn V )
56 elmapfn 
 |-  ( B e. ( R ^m V ) -> B Fn V )
57 56 ad2antll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> B Fn V )
58 53 55 57 offvalfv 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+b B ) = ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) )
59 58 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( A oF .+b B ) = ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) )
60 4 lmodfgrp 
 |-  ( M e. LMod -> S e. Grp )
61 60 grpmndd 
 |-  ( M e. LMod -> S e. Mnd )
62 61 ad3antrrr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ y e. V ) -> S e. Mnd )
63 ffvelrn 
 |-  ( ( A : V --> R /\ y e. V ) -> ( A ` y ) e. R )
64 63 ex 
 |-  ( A : V --> R -> ( y e. V -> ( A ` y ) e. R ) )
65 17 64 syl 
 |-  ( A e. ( R ^m V ) -> ( y e. V -> ( A ` y ) e. R ) )
66 65 ad2antrl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( y e. V -> ( A ` y ) e. R ) )
67 66 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ y e. V ) -> ( A ` y ) e. R )
68 4 fveq2i 
 |-  ( Base ` S ) = ( Base ` ( Scalar ` M ) )
69 5 68 eqtri 
 |-  R = ( Base ` ( Scalar ` M ) )
70 67 69 eleqtrdi 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ y e. V ) -> ( A ` y ) e. ( Base ` ( Scalar ` M ) ) )
71 ffvelrn 
 |-  ( ( B : V --> R /\ y e. V ) -> ( B ` y ) e. R )
72 71 69 eleqtrdi 
 |-  ( ( B : V --> R /\ y e. V ) -> ( B ` y ) e. ( Base ` ( Scalar ` M ) ) )
73 72 ex 
 |-  ( B : V --> R -> ( y e. V -> ( B ` y ) e. ( Base ` ( Scalar ` M ) ) ) )
74 32 73 syl 
 |-  ( B e. ( R ^m V ) -> ( y e. V -> ( B ` y ) e. ( Base ` ( Scalar ` M ) ) ) )
75 74 ad2antll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( y e. V -> ( B ` y ) e. ( Base ` ( Scalar ` M ) ) ) )
76 75 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ y e. V ) -> ( B ` y ) e. ( Base ` ( Scalar ` M ) ) )
77 4 eqcomi 
 |-  ( Scalar ` M ) = S
78 77 fveq2i 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` S )
79 78 6 mndcl 
 |-  ( ( S e. Mnd /\ ( A ` y ) e. ( Base ` ( Scalar ` M ) ) /\ ( B ` y ) e. ( Base ` ( Scalar ` M ) ) ) -> ( ( A ` y ) .+b ( B ` y ) ) e. ( Base ` ( Scalar ` M ) ) )
80 62 70 76 79 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ y e. V ) -> ( ( A ` y ) .+b ( B ` y ) ) e. ( Base ` ( Scalar ` M ) ) )
81 80 fmpttd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) : V --> ( Base ` ( Scalar ` M ) ) )
82 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
83 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P ( Base ` M ) ) -> ( ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) : V --> ( Base ` ( Scalar ` M ) ) ) )
84 82 53 83 sylancr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) : V --> ( Base ` ( Scalar ` M ) ) ) )
85 81 84 mpbird 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
86 85 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( y e. V |-> ( ( A ` y ) .+b ( B ` y ) ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
87 59 86 eqeltrd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( A oF .+b B ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
88 lincval 
 |-  ( ( M e. LMod /\ ( A oF .+b B ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( ( A oF .+b B ) ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) ) ) )
89 15 87 13 88 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( ( A oF .+b B ) ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) ) ) )
90 54 56 anim12i 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> ( A Fn V /\ B Fn V ) )
91 90 adantl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A Fn V /\ B Fn V ) )
92 91 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( A Fn V /\ B Fn V ) )
93 53 anim1i 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( V e. ~P ( Base ` M ) /\ x e. V ) )
94 fnfvof 
 |-  ( ( ( A Fn V /\ B Fn V ) /\ ( V e. ~P ( Base ` M ) /\ x e. V ) ) -> ( ( A oF .+b B ) ` x ) = ( ( A ` x ) .+b ( B ` x ) ) )
95 92 93 94 syl2anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( A oF .+b B ) ` x ) = ( ( A ` x ) .+b ( B ` x ) ) )
96 6 a1i 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> .+b = ( +g ` S ) )
97 96 oveqd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( A ` x ) .+b ( B ` x ) ) = ( ( A ` x ) ( +g ` S ) ( B ` x ) ) )
98 95 97 eqtrd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( A oF .+b B ) ` x ) = ( ( A ` x ) ( +g ` S ) ( B ` x ) ) )
99 98 oveq1d 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) = ( ( ( A ` x ) ( +g ` S ) ( B ` x ) ) ( .s ` M ) x ) )
100 14 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> M e. LMod )
101 100 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> M e. LMod )
102 20 ad2antrl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( x e. V -> ( A ` x ) e. R ) )
103 102 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( A ` x ) e. R )
104 35 ad2antll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( x e. V -> ( B ` x ) e. R ) )
105 104 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( B ` x ) e. R )
106 26 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( x e. V -> x e. ( Base ` M ) ) )
107 106 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> x e. ( Base ` M ) )
108 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
109 4 fveq2i 
 |-  ( +g ` S ) = ( +g ` ( Scalar ` M ) )
110 7 1 108 29 69 109 lmodvsdir 
 |-  ( ( M e. LMod /\ ( ( A ` x ) e. R /\ ( B ` x ) e. R /\ x e. ( Base ` M ) ) ) -> ( ( ( A ` x ) ( +g ` S ) ( B ` x ) ) ( .s ` M ) x ) = ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) )
111 101 103 105 107 110 syl13anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( ( A ` x ) ( +g ` S ) ( B ` x ) ) ( .s ` M ) x ) = ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) )
112 99 111 eqtrd 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ x e. V ) -> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) = ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) )
113 112 mpteq2dva 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( x e. V |-> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) ) = ( x e. V |-> ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) ) )
114 113 oveq2d 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( M gsum ( x e. V |-> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) ) ) = ( M gsum ( x e. V |-> ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
115 114 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( M gsum ( x e. V |-> ( ( ( A oF .+b B ) ` x ) ( .s ` M ) x ) ) ) = ( M gsum ( x e. V |-> ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
116 89 115 eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( ( A oF .+b B ) ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( ( A ` x ) ( .s ` M ) x ) .+ ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
117 2 3 oveq12i 
 |-  ( X .+ Y ) = ( ( A ( linC ` M ) V ) .+ ( B ( linC ` M ) V ) )
118 69 oveq1i 
 |-  ( R ^m V ) = ( ( Base ` ( Scalar ` M ) ) ^m V )
119 118 eleq2i 
 |-  ( A e. ( R ^m V ) <-> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
120 119 biimpi 
 |-  ( A e. ( R ^m V ) -> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
121 120 ad2antrl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
122 lincval 
 |-  ( ( M e. LMod /\ A e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( A ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) )
123 100 121 53 122 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) )
124 118 eleq2i 
 |-  ( B e. ( R ^m V ) <-> B e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
125 124 biimpi 
 |-  ( B e. ( R ^m V ) -> B e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
126 125 ad2antll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> B e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
127 lincval 
 |-  ( ( M e. LMod /\ B e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( B ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) )
128 100 126 53 127 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( B ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) )
129 123 128 oveq12d 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A ( linC ` M ) V ) .+ ( B ( linC ` M ) V ) ) = ( ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) .+ ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
130 129 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( ( A ( linC ` M ) V ) .+ ( B ( linC ` M ) V ) ) = ( ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) .+ ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
131 117 130 syl5eq 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( X .+ Y ) = ( ( M gsum ( x e. V |-> ( ( A ` x ) ( .s ` M ) x ) ) ) .+ ( M gsum ( x e. V |-> ( ( B ` x ) ( .s ` M ) x ) ) ) ) )
132 52 116 131 3eqtr4rd 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) /\ ( A finSupp ( 0g ` S ) /\ B finSupp ( 0g ` S ) ) ) -> ( X .+ Y ) = ( ( A oF .+b B ) ( linC ` M ) V ) )