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 ‘ 𝑀 )
Assertion lincsumcl ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lincsumcl.b ⊢ + = ( +g ‘ 𝑀 )
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
4 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5 2 3 4 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
6 2 3 4 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
7 5 6 anbi12d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) ↔ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
8 simpll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → 𝑀 ∈ LMod )
9 simpll ⊢ ( ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → 𝐶 ∈ ( Base ‘ 𝑀 ) )
10 9 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → 𝐶 ∈ ( Base ‘ 𝑀 ) )
11 simprl ⊢ ( ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → 𝐷 ∈ ( Base ‘ 𝑀 ) )
12 11 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → 𝐷 ∈ ( Base ‘ 𝑀 ) )
13 2 1 lmodvacl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝑀 ) )
14 8 10 12 13 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝑀 ) )
15 3 lmodfgrp ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Grp )
16 grpmnd ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Grp → ( Scalar ‘ 𝑀 ) ∈ Mnd )
17 15 16 syl ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Mnd )
18 17 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) ∈ Mnd )
19 18 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( Scalar ‘ 𝑀 ) ∈ Mnd )
20 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
21 20 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
22 simpll ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
23 simpl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
24 22 23 anim12i ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) )
25 24 adantr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) )
26 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
27 4 26 ofaddmndmap ⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
28 19 21 25 27 syl3anc ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
29 17 anim1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
30 29 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
31 simprl ⊢ ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
32 31 adantr ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
33 simprl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
34 32 33 anim12i ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
35 34 adantr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
36 4 mndpfsupp ⊢ ( ( ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
37 30 25 35 36 syl3anc ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
38 oveq12 ⊢ ( ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
39 38 expcom ⊢ ( 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
40 39 adantl ⊢ ( ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
41 40 adantl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
42 41 com12 ⊢ ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
43 42 adantl ⊢ ( ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
44 43 adantl ⊢ ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
45 44 adantr ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
46 45 imp ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
47 46 adantr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
48 simpr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
49 eqid ⊢ ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 )
50 eqid ⊢ ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 )
51 1 49 50 3 4 26 lincsum ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
52 48 25 35 51 syl3anc ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
53 47 52 eqtrd ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
54 breq1 ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
55 oveq1 ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
56 55 eqeq2d ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) )
57 54 56 anbi12d ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
58 57 rspcev ⊢ ( ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
59 28 37 53 58 syl12anc ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
60 59 exp41 ⊢ ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
61 60 rexlimiva ⊢ ( ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
62 61 expd ⊢ ( ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 ∈ ( Base ‘ 𝑀 ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) ) )
63 62 impcom ⊢ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
64 63 com13 ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
65 64 rexlimiva ⊢ ( ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
66 65 impcom ⊢ ( ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
67 66 impcom ⊢ ( ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
68 67 impcom ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
69 2 3 4 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
70 69 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → ( ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
71 14 68 70 mpbir2and ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )
72 71 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
73 7 72 sylbid ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
74 73 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )