Metamath Proof Explorer

Theorem lincscmcl

Description: The multiplication of a linear combination with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 11-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses lincscmcl.s 
|- .x. = ( .s ` M )
lincscmcl.r 
|- R = ( Base ` ( Scalar ` M ) )
Assertion lincscmcl 
|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R /\ D e. ( M LinCo V ) ) -> ( C .x. D ) e. ( M LinCo V ) )

Proof

Step Hyp Ref Expression
1 lincscmcl.s 
 |-  .x. = ( .s ` M )
2 lincscmcl.r 
 |-  R = ( Base ` ( Scalar ` M ) )
3 eqid 
 |-  ( Base ` M ) = ( Base ` M )
4 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
5 3 4 2 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( D e. ( M LinCo V ) <-> ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) )
6 5 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> ( D e. ( M LinCo V ) <-> ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) )
7 simpl 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> M e. LMod )
8 7 ad2antrr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> M e. LMod )
9 simpr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> C e. R )
10 9 adantr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> C e. R )
11 simprl 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> D e. ( Base ` M ) )
12 3 4 1 2 lmodvscl 
 |-  ( ( M e. LMod /\ C e. R /\ D e. ( Base ` M ) ) -> ( C .x. D ) e. ( Base ` M ) )
13 8 10 11 12 syl3anc 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( C .x. D ) e. ( Base ` M ) )
14 4 lmodring 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Ring )
15 14 ad2antrr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> ( Scalar ` M ) e. Ring )
16 15 adantl 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( Scalar ` M ) e. Ring )
17 16 adantr 
 |-  ( ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) /\ v e. V ) -> ( Scalar ` M ) e. Ring )
18 9 adantl 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> C e. R )
19 18 adantr 
 |-  ( ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) /\ v e. V ) -> C e. R )
20 elmapi 
 |-  ( x e. ( R ^m V ) -> x : V --> R )
21 ffvelrn 
 |-  ( ( x : V --> R /\ v e. V ) -> ( x ` v ) e. R )
22 21 ex 
 |-  ( x : V --> R -> ( v e. V -> ( x ` v ) e. R ) )
23 20 22 syl 
 |-  ( x e. ( R ^m V ) -> ( v e. V -> ( x ` v ) e. R ) )
24 23 adantr 
 |-  ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( v e. V -> ( x ` v ) e. R ) )
25 24 ad2antrr 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( v e. V -> ( x ` v ) e. R ) )
26 25 imp 
 |-  ( ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) /\ v e. V ) -> ( x ` v ) e. R )
27 eqid 
 |-  ( .r ` ( Scalar ` M ) ) = ( .r ` ( Scalar ` M ) )
28 2 27 ringcl 
 |-  ( ( ( Scalar ` M ) e. Ring /\ C e. R /\ ( x ` v ) e. R ) -> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) e. R )
29 17 19 26 28 syl3anc 
 |-  ( ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) /\ v e. V ) -> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) e. R )
30 29 fmpttd 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) : V --> R )
31 2 fvexi 
 |-  R e. _V
32 simpr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
33 32 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> V e. ~P ( Base ` M ) )
34 33 adantl 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> V e. ~P ( Base ` M ) )
35 elmapg 
 |-  ( ( R e. _V /\ V e. ~P ( Base ` M ) ) -> ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) e. ( R ^m V ) <-> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) : V --> R ) )
36 31 34 35 sylancr 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) e. ( R ^m V ) <-> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) : V --> R ) )
37 30 36 mpbird 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) e. ( R ^m V ) )
38 15 33 9 3jca 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> ( ( Scalar ` M ) e. Ring /\ V e. ~P ( Base ` M ) /\ C e. R ) )
39 38 adantl 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( ( Scalar ` M ) e. Ring /\ V e. ~P ( Base ` M ) /\ C e. R ) )
40 simpl 
 |-  ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> x e. ( R ^m V ) )
41 40 ad2antrr 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> x e. ( R ^m V ) )
42 simprl 
 |-  ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> x finSupp ( 0g ` ( Scalar ` M ) ) )
43 42 ad2antrr 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> x finSupp ( 0g ` ( Scalar ` M ) ) )
44 2 rmfsupp 
 |-  ( ( ( ( Scalar ` M ) e. Ring /\ V e. ~P ( Base ` M ) /\ C e. R ) /\ x e. ( R ^m V ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
45 39 41 43 44 syl3anc 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) )
46 oveq2 
 |-  ( D = ( x ( linC ` M ) V ) -> ( C .x. D ) = ( C .x. ( x ( linC ` M ) V ) ) )
47 46 adantl 
 |-  ( ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) -> ( C .x. D ) = ( C .x. ( x ( linC ` M ) V ) ) )
48 47 adantl 
 |-  ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .x. D ) = ( C .x. ( x ( linC ` M ) V ) ) )
49 48 ad2antrr 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( C .x. D ) = ( C .x. ( x ( linC ` M ) V ) ) )
50 simprl 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
51 40 adantr 
 |-  ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) -> x e. ( R ^m V ) )
52 51 9 anim12i 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( x e. ( R ^m V ) /\ C e. R ) )
53 eqid 
 |-  ( x ( linC ` M ) V ) = ( x ( linC ` M ) V )
54 eqid 
 |-  ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) = ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) )
55 1 27 53 2 54 lincscm 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( x e. ( R ^m V ) /\ C e. R ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) -> ( C .x. ( x ( linC ` M ) V ) ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) )
56 50 52 43 55 syl3anc 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( C .x. ( x ( linC ` M ) V ) ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) )
57 49 56 eqtrd 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> ( C .x. D ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) )
58 breq1 
 |-  ( s = ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) -> ( s finSupp ( 0g ` ( Scalar ` M ) ) <-> ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) ) )
59 oveq1 
 |-  ( s = ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) -> ( s ( linC ` M ) V ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) )
60 59 eqeq2d 
 |-  ( s = ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) -> ( ( C .x. D ) = ( s ( linC ` M ) V ) <-> ( C .x. D ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) ) )
61 58 60 anbi12d 
 |-  ( s = ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) -> ( ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) <-> ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) ) ) )
62 61 rspcev 
 |-  ( ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) e. ( R ^m V ) /\ ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( ( v e. V |-> ( C ( .r ` ( Scalar ` M ) ) ( x ` v ) ) ) ( linC ` M ) V ) ) ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) )
63 37 45 57 62 syl12anc 
 |-  ( ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) /\ ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) )
64 63 ex 
 |-  ( ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) /\ D e. ( Base ` M ) ) -> ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) )
65 64 ex 
 |-  ( ( x e. ( R ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( D e. ( Base ` M ) -> ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) ) )
66 65 rexlimiva 
 |-  ( E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) -> ( D e. ( Base ` M ) -> ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) ) )
67 66 impcom 
 |-  ( ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) )
68 67 impcom 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) )
69 3 4 2 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( C .x. D ) e. ( M LinCo V ) <-> ( ( C .x. D ) e. ( Base ` M ) /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) ) )
70 69 ad2antrr 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( ( C .x. D ) e. ( M LinCo V ) <-> ( ( C .x. D ) e. ( Base ` M ) /\ E. s e. ( R ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .x. D ) = ( s ( linC ` M ) V ) ) ) ) )
71 13 68 70 mpbir2and 
 |-  ( ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) /\ ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( C .x. D ) e. ( M LinCo V ) )
72 71 ex 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> ( ( D e. ( Base ` M ) /\ E. x e. ( R ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .x. D ) e. ( M LinCo V ) ) )
73 6 72 sylbid 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R ) -> ( D e. ( M LinCo V ) -> ( C .x. D ) e. ( M LinCo V ) ) )
74 73 3impia 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ C e. R /\ D e. ( M LinCo V ) ) -> ( C .x. D ) e. ( M LinCo V ) )