Metamath Proof Explorer

Theorem lincsum

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

Ref Expression
Hypotheses lincsum.p ⊢ + = ( +g ‘ 𝑀 )
lincsum.x ⊢ 𝑋 = ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 )
lincsum.y ⊢ 𝑌 = ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 )
lincsum.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lincsum.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
lincsum.b ⊢ ✚ = ( +g ‘ 𝑆 )
Assertion lincsum ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lincsum.p ⊢ + = ( +g ‘ 𝑀 )
2 lincsum.x ⊢ 𝑋 = ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 )
3 lincsum.y ⊢ 𝑌 = ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 )
4 lincsum.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5 lincsum.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
6 lincsum.b ⊢ ✚ = ( +g ‘ 𝑆 )
7 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
8 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
9 lmodcmn ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
10 9 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑀 ∈ CMnd )
11 10 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → 𝑀 ∈ CMnd )
12 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
13 12 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
14 simpl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LMod )
15 14 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → 𝑀 ∈ LMod )
16 15 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑀 ∈ LMod )
17 elmapi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
18 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
19 18 ex ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
20 17 19 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
22 21 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
23 22 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
24 elelpwi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
25 24 expcom ⊢ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
26 25 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
27 26 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
28 27 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
29 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
30 7 4 29 5 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
31 16 23 28 30 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
32 elmapi ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 : 𝑉 ⟶ 𝑅 )
33 ffvelrn ⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
34 33 ex ⊢ ( 𝐵 : 𝑉 ⟶ 𝑅 → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
35 32 34 syl ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
36 35 adantl ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
37 36 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
38 37 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
39 7 4 29 5 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
40 16 38 28 39 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ ( Base ‘ 𝑀 ) )
41 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
42 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
43 id ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
44 simpl ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) )
45 simpl ⊢ ( ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) → 𝐴 finSupp ( 0g ‘ 𝑆 ) )
46 4 5 scmfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐴 finSupp ( 0g ‘ 𝑆 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0g ‘ 𝑀 ) )
47 43 44 45 46 syl3an ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0g ‘ 𝑀 ) )
48 simpr ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) )
49 simpr ⊢ ( ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) → 𝐵 finSupp ( 0g ‘ 𝑆 ) )
50 4 5 scmfsupp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0g ‘ 𝑀 ) )
51 43 48 49 50 syl3an ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) finSupp ( 0g ‘ 𝑀 ) )
52 7 8 1 11 13 31 40 41 42 47 51 gsummptfsadd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
53 12 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
54 elmapfn ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 Fn 𝑉 )
55 54 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐴 Fn 𝑉 )
56 elmapfn ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 Fn 𝑉 )
57 56 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 Fn 𝑉 )
58 53 55 57 offvalfv ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f ✚ 𝐵 ) = ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) )
59 58 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝐴 ∘f ✚ 𝐵 ) = ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) )
60 4 lmodfgrp ⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Grp )
61 60 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Mnd )
62 61 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝑆 ∈ Mnd )
63 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 )
64 63 ex ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
65 17 64 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
66 65 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
67 66 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 )
68 4 fveq2i ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
69 5 68 eqtri ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
70 67 69 eleqtrdi ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
71 ffvelrn ⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ 𝑅 )
72 71 69 eleqtrdi ⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
73 72 ex ⊢ ( 𝐵 : 𝑉 ⟶ 𝑅 → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
74 32 73 syl ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
75 74 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
76 75 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
77 4 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = 𝑆
78 77 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
79 78 6 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 𝐴 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
80 62 70 76 79 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
81 80 fmpttd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
82 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
83 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
84 82 53 83 sylancr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
85 81 84 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
86 85 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
87 59 86 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝐴 ∘f ✚ 𝐵 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
88 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐴 ∘f ✚ 𝐵 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
89 15 87 13 88 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
90 54 56 anim12i ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
91 90 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
92 91 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
93 53 anim1i ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑉 ) )
94 fnfvof ⊢ ( ( ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) )
95 92 93 94 syl2anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) )
96 6 a1i ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ✚ = ( +g ‘ 𝑆 ) )
97 96 oveqd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) )
98 95 97 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) )
99 98 oveq1d ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
100 14 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑀 ∈ LMod )
101 100 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑀 ∈ LMod )
102 20 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
103 102 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
104 35 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
105 104 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
106 26 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
107 106 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
108 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
109 4 fveq2i ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
110 7 1 108 29 69 109 lmodvsdir ⊢ ( ( 𝑀 ∈ LMod ∧ ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ∧ ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
111 101 103 105 107 110 syl13anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
112 99 111 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
113 112 mpteq2dva ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
114 113 oveq2d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
115 114 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
116 89 115 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
117 2 3 oveq12i ⊢ ( 𝑋 + 𝑌 ) = ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) )
118 69 oveq1i ⊢ ( 𝑅 ↑m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 )
119 118 eleq2i ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
120 119 biimpi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
121 120 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
122 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
123 100 121 53 122 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
124 118 eleq2i ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
125 124 biimpi ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
126 125 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
127 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
128 100 126 53 127 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
129 123 128 oveq12d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
130 129 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
131 117 130 syl5eq ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
132 52 116 131 3eqtr4rd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) )