Metamath Proof Explorer

Theorem lincsumcl

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) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypothesis lincsumcl.b 
|- .+ = ( +g ` M )
Assertion lincsumcl 
|- ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. ( M LinCo V ) /\ D e. ( M LinCo V ) ) ) -> ( C .+ D ) e. ( M LinCo V ) )

Proof

Step Hyp Ref Expression
1 lincsumcl.b 
 |-  .+ = ( +g ` M )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
4 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
5 2 3 4 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( C e. ( M LinCo V ) <-> ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) ) )
6 2 3 4 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( D e. ( M LinCo V ) <-> ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) )
7 5 6 anbi12d 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( C e. ( M LinCo V ) /\ D e. ( M LinCo V ) ) <-> ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) )
8 simpll 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> M e. LMod )
9 simpll 
 |-  ( ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> C e. ( Base ` M ) )
10 9 adantl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> C e. ( Base ` M ) )
11 simprl 
 |-  ( ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> D e. ( Base ` M ) )
12 11 adantl 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> D e. ( Base ` M ) )
13 2 1 lmodvacl 
 |-  ( ( M e. LMod /\ C e. ( Base ` M ) /\ D e. ( Base ` M ) ) -> ( C .+ D ) e. ( Base ` M ) )
14 8 10 12 13 syl3anc 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> ( C .+ D ) e. ( Base ` M ) )
15 3 lmodfgrp 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Grp )
16 15 grpmndd 
 |-  ( M e. LMod -> ( Scalar ` M ) e. Mnd )
17 16 adantr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( Scalar ` M ) e. Mnd )
18 17 adantl 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( Scalar ` M ) e. Mnd )
19 simpr 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
20 19 adantl 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> V e. ~P ( Base ` M ) )
21 simpll 
 |-  ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) -> y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
22 simpl 
 |-  ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
23 21 22 anim12i 
 |-  ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ) )
24 23 adantr 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ) )
25 eqid 
 |-  ( +g ` ( Scalar ` M ) ) = ( +g ` ( Scalar ` M ) )
26 4 25 ofaddmndmap 
 |-  ( ( ( Scalar ` M ) e. Mnd /\ V e. ~P ( Base ` M ) /\ ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ) ) -> ( y oF ( +g ` ( Scalar ` M ) ) x ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
27 18 20 24 26 syl3anc 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( y oF ( +g ` ( Scalar ` M ) ) x ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
28 16 anim1i 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( Scalar ` M ) e. Mnd /\ V e. ~P ( Base ` M ) ) )
29 28 adantl 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( ( Scalar ` M ) e. Mnd /\ V e. ~P ( Base ` M ) ) )
30 simprl 
 |-  ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> y finSupp ( 0g ` ( Scalar ` M ) ) )
31 30 adantr 
 |-  ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) -> y finSupp ( 0g ` ( Scalar ` M ) ) )
32 simprl 
 |-  ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> x finSupp ( 0g ` ( Scalar ` M ) ) )
33 31 32 anim12i 
 |-  ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) )
34 33 adantr 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) )
35 4 mndpfsupp 
 |-  ( ( ( ( Scalar ` M ) e. Mnd /\ V e. ~P ( Base ` M ) ) /\ ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> ( y oF ( +g ` ( Scalar ` M ) ) x ) finSupp ( 0g ` ( Scalar ` M ) ) )
36 29 24 34 35 syl3anc 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( y oF ( +g ` ( Scalar ` M ) ) x ) finSupp ( 0g ` ( Scalar ` M ) ) )
37 oveq12 
 |-  ( ( C = ( y ( linC ` M ) V ) /\ D = ( x ( linC ` M ) V ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) )
38 37 expcom 
 |-  ( D = ( x ( linC ` M ) V ) -> ( C = ( y ( linC ` M ) V ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
39 38 adantl 
 |-  ( ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) -> ( C = ( y ( linC ` M ) V ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
40 39 adantl 
 |-  ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C = ( y ( linC ` M ) V ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
41 40 com12 
 |-  ( C = ( y ( linC ` M ) V ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
42 41 adantl 
 |-  ( ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
43 42 adantl 
 |-  ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
44 43 adantr 
 |-  ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) ) )
45 44 imp 
 |-  ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) )
46 45 adantr 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( C .+ D ) = ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) )
47 simpr 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( M e. LMod /\ V e. ~P ( Base ` M ) ) )
48 eqid 
 |-  ( y ( linC ` M ) V ) = ( y ( linC ` M ) V )
49 eqid 
 |-  ( x ( linC ` M ) V ) = ( x ( linC ` M ) V )
50 1 48 49 3 4 25 lincsum 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ x finSupp ( 0g ` ( Scalar ` M ) ) ) ) -> ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) )
51 47 24 34 50 syl3anc 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( ( y ( linC ` M ) V ) .+ ( x ( linC ` M ) V ) ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) )
52 46 51 eqtrd 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> ( C .+ D ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) )
53 breq1 
 |-  ( s = ( y oF ( +g ` ( Scalar ` M ) ) x ) -> ( s finSupp ( 0g ` ( Scalar ` M ) ) <-> ( y oF ( +g ` ( Scalar ` M ) ) x ) finSupp ( 0g ` ( Scalar ` M ) ) ) )
54 oveq1 
 |-  ( s = ( y oF ( +g ` ( Scalar ` M ) ) x ) -> ( s ( linC ` M ) V ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) )
55 54 eqeq2d 
 |-  ( s = ( y oF ( +g ` ( Scalar ` M ) ) x ) -> ( ( C .+ D ) = ( s ( linC ` M ) V ) <-> ( C .+ D ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) ) )
56 53 55 anbi12d 
 |-  ( s = ( y oF ( +g ` ( Scalar ` M ) ) x ) -> ( ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) <-> ( ( y oF ( +g ` ( Scalar ` M ) ) x ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) ) ) )
57 56 rspcev 
 |-  ( ( ( y oF ( +g ` ( Scalar ` M ) ) x ) e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( ( y oF ( +g ` ( Scalar ` M ) ) x ) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( ( y oF ( +g ` ( Scalar ` M ) ) x ) ( linC ` M ) V ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) )
58 27 36 52 57 syl12anc 
 |-  ( ( ( ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) ) /\ ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) /\ ( M e. LMod /\ V e. ~P ( Base ` M ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) )
59 58 exp41 
 |-  ( ( y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) )
60 59 rexlimiva 
 |-  ( E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) -> ( ( C e. ( Base ` M ) /\ D e. ( Base ` M ) ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) )
61 60 expd 
 |-  ( E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) -> ( C e. ( Base ` M ) -> ( D e. ( Base ` M ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) ) )
62 61 impcom 
 |-  ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( D e. ( Base ` M ) -> ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) )
63 62 com13 
 |-  ( ( x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( D e. ( Base ` M ) -> ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) )
64 63 rexlimiva 
 |-  ( E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) -> ( D e. ( Base ` M ) -> ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) ) )
65 64 impcom 
 |-  ( ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) -> ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) )
66 65 impcom 
 |-  ( ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) )
67 66 impcom 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) )
68 2 3 4 lcoval 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( C .+ D ) e. ( M LinCo V ) <-> ( ( C .+ D ) e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) )
69 68 adantr 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> ( ( C .+ D ) e. ( M LinCo V ) <-> ( ( C .+ D ) e. ( Base ` M ) /\ E. s e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( s finSupp ( 0g ` ( Scalar ` M ) ) /\ ( C .+ D ) = ( s ( linC ` M ) V ) ) ) ) )
70 14 67 69 mpbir2and 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) ) -> ( C .+ D ) e. ( M LinCo V ) )
71 70 ex 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( ( C e. ( Base ` M ) /\ E. y e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( y finSupp ( 0g ` ( Scalar ` M ) ) /\ C = ( y ( linC ` M ) V ) ) ) /\ ( D e. ( Base ` M ) /\ E. x e. ( ( Base ` ( Scalar ` M ) ) ^m V ) ( x finSupp ( 0g ` ( Scalar ` M ) ) /\ D = ( x ( linC ` M ) V ) ) ) ) -> ( C .+ D ) e. ( M LinCo V ) ) )
72 7 71 sylbid 
 |-  ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) -> ( ( C e. ( M LinCo V ) /\ D e. ( M LinCo V ) ) -> ( C .+ D ) e. ( M LinCo V ) ) )
73 72 imp 
 |-  ( ( ( M e. LMod /\ V e. ~P ( Base ` M ) ) /\ ( C e. ( M LinCo V ) /\ D e. ( M LinCo V ) ) ) -> ( C .+ D ) e. ( M LinCo V ) )