Metamath Proof Explorer

Theorem lincdifsn

Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincdifsn.b 
|- B = ( Base ` M )
lincdifsn.r 
|- R = ( Scalar ` M )
lincdifsn.s 
|- S = ( Base ` R )
lincdifsn.t 
|- .x. = ( .s ` M )
lincdifsn.p 
|- .+ = ( +g ` M )
lincdifsn.0 
|- .0. = ( 0g ` R )
Assertion lincdifsn 
|- ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( F ( linC ` M ) V ) = ( ( G ( linC ` M ) ( V \ { X } ) ) .+ ( ( F ` X ) .x. X ) ) )

Proof

Step Hyp Ref Expression
1 lincdifsn.b 
 |-  B = ( Base ` M )
2 lincdifsn.r 
 |-  R = ( Scalar ` M )
3 lincdifsn.s 
 |-  S = ( Base ` R )
4 lincdifsn.t 
 |-  .x. = ( .s ` M )
5 lincdifsn.p 
 |-  .+ = ( +g ` M )
6 lincdifsn.0 
 |-  .0. = ( 0g ` R )
7 simp11 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> M e. LMod )
8 2 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
9 3 8 eqtri 
 |-  S = ( Base ` ( Scalar ` M ) )
10 9 oveq1i 
 |-  ( S ^m V ) = ( ( Base ` ( Scalar ` M ) ) ^m V )
11 10 eleq2i 
 |-  ( F e. ( S ^m V ) <-> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
12 11 biimpi 
 |-  ( F e. ( S ^m V ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
13 12 adantr 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
14 13 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
15 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
16 15 eleq2i 
 |-  ( V e. ~P B <-> V e. ~P ( Base ` M ) )
17 16 biimpi 
 |-  ( V e. ~P B -> V e. ~P ( Base ` M ) )
18 17 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> V e. ~P ( Base ` M ) )
19 18 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> 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 ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) ) )
21 7 14 19 20 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) ) )
22 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
23 22 3ad2ant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> M e. CMnd )
24 23 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> M e. CMnd )
25 simp12 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> V e. ~P B )
26 17 anim2i 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
27 26 3adant3 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
28 27 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
29 simp2l 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> F e. ( S ^m V ) )
30 6 breq2i 
 |-  ( F finSupp .0. <-> F finSupp ( 0g ` R ) )
31 30 biimpi 
 |-  ( F finSupp .0. -> F finSupp ( 0g ` R ) )
32 31 adantl 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> F finSupp ( 0g ` R ) )
33 32 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> F finSupp ( 0g ` R ) )
34 2 3 scmfsupp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ F e. ( S ^m V ) /\ F finSupp ( 0g ` R ) ) -> ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
35 28 29 33 34 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) finSupp ( 0g ` M ) )
36 simpl1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> M e. LMod )
37 36 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ x e. V ) -> M e. LMod )
38 elmapi 
 |-  ( F e. ( S ^m V ) -> F : V --> S )
39 ffvelrn 
 |-  ( ( F : V --> S /\ x e. V ) -> ( F ` x ) e. S )
40 39 ex 
 |-  ( F : V --> S -> ( x e. V -> ( F ` x ) e. S ) )
41 40 a1d 
 |-  ( F : V --> S -> ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( x e. V -> ( F ` x ) e. S ) ) )
42 38 41 syl 
 |-  ( F e. ( S ^m V ) -> ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( x e. V -> ( F ` x ) e. S ) ) )
43 42 adantr 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( x e. V -> ( F ` x ) e. S ) ) )
44 43 impcom 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( x e. V -> ( F ` x ) e. S ) )
45 44 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ x e. V ) -> ( F ` x ) e. S )
46 elelpwi 
 |-  ( ( x e. V /\ V e. ~P B ) -> x e. B )
47 46 expcom 
 |-  ( V e. ~P B -> ( x e. V -> x e. B ) )
48 47 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( x e. V -> x e. B ) )
49 48 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( x e. V -> x e. B ) )
50 49 imp 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ x e. V ) -> x e. B )
51 eqid 
 |-  ( .s ` M ) = ( .s ` M )
52 1 2 51 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` x ) e. S /\ x e. B ) -> ( ( F ` x ) ( .s ` M ) x ) e. B )
53 37 45 50 52 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) /\ x e. V ) -> ( ( F ` x ) ( .s ` M ) x ) e. B )
54 53 3adantl3 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) /\ x e. V ) -> ( ( F ` x ) ( .s ` M ) x ) e. B )
55 simp13 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> X e. V )
56 ffvelrn 
 |-  ( ( F : V --> S /\ X e. V ) -> ( F ` X ) e. S )
57 56 expcom 
 |-  ( X e. V -> ( F : V --> S -> ( F ` X ) e. S ) )
58 57 3ad2ant3 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F : V --> S -> ( F ` X ) e. S ) )
59 38 58 syl5com 
 |-  ( F e. ( S ^m V ) -> ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ` X ) e. S ) )
60 59 adantr 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( F ` X ) e. S ) )
61 60 impcom 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( F ` X ) e. S )
62 elelpwi 
 |-  ( ( X e. V /\ V e. ~P B ) -> X e. B )
63 62 ancoms 
 |-  ( ( V e. ~P B /\ X e. V ) -> X e. B )
64 63 3adant1 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> X e. B )
65 64 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> X e. B )
66 1 2 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ ( F ` X ) e. S /\ X e. B ) -> ( ( F ` X ) .x. X ) e. B )
67 36 61 65 66 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) ) -> ( ( F ` X ) .x. X ) e. B )
68 67 3adant3 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( ( F ` X ) .x. X ) e. B )
69 4 eqcomi 
 |-  ( .s ` M ) = .x.
70 69 a1i 
 |-  ( x = X -> ( .s ` M ) = .x. )
71 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
72 id 
 |-  ( x = X -> x = X )
73 70 71 72 oveq123d 
 |-  ( x = X -> ( ( F ` x ) ( .s ` M ) x ) = ( ( F ` X ) .x. X ) )
74 73 adantl 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) /\ x = X ) -> ( ( F ` x ) ( .s ` M ) x ) = ( ( F ` X ) .x. X ) )
75 1 5 24 25 35 54 55 68 74 gsumdifsnd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( M gsum ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) ) = ( ( M gsum ( x e. ( V \ { X } ) |-> ( ( F ` x ) ( .s ` M ) x ) ) ) .+ ( ( F ` X ) .x. X ) ) )
76 fveq1 
 |-  ( G = ( F |` ( V \ { X } ) ) -> ( G ` x ) = ( ( F |` ( V \ { X } ) ) ` x ) )
77 76 3ad2ant3 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( G ` x ) = ( ( F |` ( V \ { X } ) ) ` x ) )
78 fvres 
 |-  ( x e. ( V \ { X } ) -> ( ( F |` ( V \ { X } ) ) ` x ) = ( F ` x ) )
79 77 78 sylan9eq 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) /\ x e. ( V \ { X } ) ) -> ( G ` x ) = ( F ` x ) )
80 79 oveq1d 
 |-  ( ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) /\ x e. ( V \ { X } ) ) -> ( ( G ` x ) ( .s ` M ) x ) = ( ( F ` x ) ( .s ` M ) x ) )
81 80 mpteq2dva 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) = ( x e. ( V \ { X } ) |-> ( ( F ` x ) ( .s ` M ) x ) ) )
82 81 eqcomd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( x e. ( V \ { X } ) |-> ( ( F ` x ) ( .s ` M ) x ) ) = ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) )
83 82 oveq2d 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( M gsum ( x e. ( V \ { X } ) |-> ( ( F ` x ) ( .s ` M ) x ) ) ) = ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) )
84 83 oveq1d 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( ( M gsum ( x e. ( V \ { X } ) |-> ( ( F ` x ) ( .s ` M ) x ) ) ) .+ ( ( F ` X ) .x. X ) ) = ( ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) .+ ( ( F ` X ) .x. X ) ) )
85 75 84 eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( M gsum ( x e. V |-> ( ( F ` x ) ( .s ` M ) x ) ) ) = ( ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) .+ ( ( F ` X ) .x. X ) ) )
86 eqid 
 |-  V = V
87 86 9 feq23i 
 |-  ( F : V --> S <-> F : V --> ( Base ` ( Scalar ` M ) ) )
88 38 87 sylib 
 |-  ( F e. ( S ^m V ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
89 88 adantr 
 |-  ( ( F e. ( S ^m V ) /\ F finSupp .0. ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
90 89 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
91 difssd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( V \ { X } ) C_ V )
92 90 91 fssresd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( F |` ( V \ { X } ) ) : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) )
93 feq1 
 |-  ( G = ( F |` ( V \ { X } ) ) -> ( G : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) <-> ( F |` ( V \ { X } ) ) : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
94 93 3ad2ant3 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( G : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) <-> ( F |` ( V \ { X } ) ) : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
95 92 94 mpbird 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> G : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) )
96 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
97 difexg 
 |-  ( V e. ~P B -> ( V \ { X } ) e. _V )
98 97 3ad2ant2 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( V \ { X } ) e. _V )
99 98 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( V \ { X } ) e. _V )
100 elmapg 
 |-  ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ ( V \ { X } ) e. _V ) -> ( G e. ( ( Base ` ( Scalar ` M ) ) ^m ( V \ { X } ) ) <-> G : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
101 96 99 100 sylancr 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( G e. ( ( Base ` ( Scalar ` M ) ) ^m ( V \ { X } ) ) <-> G : ( V \ { X } ) --> ( Base ` ( Scalar ` M ) ) ) )
102 95 101 mpbird 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> G e. ( ( Base ` ( Scalar ` M ) ) ^m ( V \ { X } ) ) )
103 elpwi 
 |-  ( V e. ~P B -> V C_ B )
104 1 sseq2i 
 |-  ( V C_ B <-> V C_ ( Base ` M ) )
105 104 biimpi 
 |-  ( V C_ B -> V C_ ( Base ` M ) )
106 105 ssdifssd 
 |-  ( V C_ B -> ( V \ { X } ) C_ ( Base ` M ) )
107 103 106 syl 
 |-  ( V e. ~P B -> ( V \ { X } ) C_ ( Base ` M ) )
108 107 adantl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( V \ { X } ) C_ ( Base ` M ) )
109 97 adantl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( V \ { X } ) e. _V )
110 elpwg 
 |-  ( ( V \ { X } ) e. _V -> ( ( V \ { X } ) e. ~P ( Base ` M ) <-> ( V \ { X } ) C_ ( Base ` M ) ) )
111 109 110 syl 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( ( V \ { X } ) e. ~P ( Base ` M ) <-> ( V \ { X } ) C_ ( Base ` M ) ) )
112 108 111 mpbird 
 |-  ( ( M e. LMod /\ V e. ~P B ) -> ( V \ { X } ) e. ~P ( Base ` M ) )
113 112 3adant3 
 |-  ( ( M e. LMod /\ V e. ~P B /\ X e. V ) -> ( V \ { X } ) e. ~P ( Base ` M ) )
114 113 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( V \ { X } ) e. ~P ( Base ` M ) )
115 lincval 
 |-  ( ( M e. LMod /\ G e. ( ( Base ` ( Scalar ` M ) ) ^m ( V \ { X } ) ) /\ ( V \ { X } ) e. ~P ( Base ` M ) ) -> ( G ( linC ` M ) ( V \ { X } ) ) = ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) )
116 7 102 114 115 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( G ( linC ` M ) ( V \ { X } ) ) = ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) )
117 116 eqcomd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) = ( G ( linC ` M ) ( V \ { X } ) ) )
118 117 oveq1d 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( ( M gsum ( x e. ( V \ { X } ) |-> ( ( G ` x ) ( .s ` M ) x ) ) ) .+ ( ( F ` X ) .x. X ) ) = ( ( G ( linC ` M ) ( V \ { X } ) ) .+ ( ( F ` X ) .x. X ) ) )
119 21 85 118 3eqtrd 
 |-  ( ( ( M e. LMod /\ V e. ~P B /\ X e. V ) /\ ( F e. ( S ^m V ) /\ F finSupp .0. ) /\ G = ( F |` ( V \ { X } ) ) ) -> ( F ( linC ` M ) V ) = ( ( G ( linC ` M ) ( V \ { X } ) ) .+ ( ( F ` X ) .x. X ) ) )