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 15 grpmndd ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Mnd )
17 16 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) ∈ Mnd )
18 17 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( Scalar ‘ 𝑀 ) ∈ Mnd )
19 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
20 19 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
21 simpll ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
22 simpl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
23 21 22 anim12i ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) )
24 23 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 𝑉 ) ) )
25 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
26 4 25 ofaddmndmap ⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
27 18 20 24 26 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 𝑉 ) )
28 16 anim1i ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
29 28 adantl ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
30 simprl ⊢ ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
31 30 adantr ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
32 simprl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
33 31 32 anim12i ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
34 33 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 ‘ 𝑀 ) ) ) )
35 4 mndpfsupp ⊢ ( ( ( ( Scalar ‘ 𝑀 ) ∈ Mnd ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
36 29 24 34 35 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 ‘ 𝑀 ) ) )
37 oveq12 ⊢ ( ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
38 37 expcom ⊢ ( 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
39 38 adantl ⊢ ( ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
40 39 adantl ⊢ ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
41 40 com12 ⊢ ( 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
42 41 adantl ⊢ ( ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
43 42 adantl ⊢ ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
44 43 adantr ⊢ ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
45 44 imp ⊢ ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
46 45 adantr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
47 simpr ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
48 eqid ⊢ ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 )
49 eqid ⊢ ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 )
50 1 48 49 3 4 25 lincsum ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
51 47 24 34 50 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 ‘ 𝑀 ) 𝑉 ) )
52 46 51 eqtrd ⊢ ( ( ( ( ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ) ∧ ( 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
53 breq1 ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
54 oveq1 ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) )
55 54 eqeq2d ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) )
56 53 55 anbi12d ⊢ ( 𝑠 = ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
57 56 rspcev ⊢ ( ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( ( 𝑦 ∘f ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑥 ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
58 27 36 52 57 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 ‘ 𝑀 ) 𝑉 ) ) )
59 58 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
60 59 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
61 60 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) ) )
62 61 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
63 62 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
64 63 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 ‘ 𝑀 ) 𝑉 ) ) ) ) ) )
65 64 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 ‘ 𝑀 ) 𝑉 ) ) ) ) )
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 ⊢ ( ( ( 𝑀 ∈ 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 ‘ 𝑀 ) 𝑉 ) ) )
68 2 3 4 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 + 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
69 68 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 ‘ 𝑀 ) 𝑉 ) ) ) ) )
70 14 67 69 mpbir2and ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )
71 70 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( ( 𝐶 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑦 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐶 = ( 𝑦 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
72 7 71 sylbid ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
73 72 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐶 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( 𝐶 + 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )