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 grpmnd ⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
62 60 61 syl ⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Mnd )
63 62 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝑆 ∈ Mnd )
64 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 )
65 64 ex ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
66 17 65 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
67 66 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 ) )
68 67 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 )
69 4 fveq2i ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
70 5 69 eqtri ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
71 68 70 eleqtrdi ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
72 ffvelrn ⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ 𝑅 )
73 72 70 eleqtrdi ⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
74 73 ex ⊢ ( 𝐵 : 𝑉 ⟶ 𝑅 → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
75 32 74 syl ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
76 75 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
77 76 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
78 4 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = 𝑆
79 78 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
80 79 6 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 𝐴 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐵 ‘ 𝑦 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
81 63 71 77 80 syl3anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
82 81 fmpttd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
83 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
84 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
85 83 53 84 sylancr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
86 82 85 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
87 86 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑦 ) ✚ ( 𝐵 ‘ 𝑦 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
88 59 87 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝐴 ∘f ✚ 𝐵 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
89 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐴 ∘f ✚ 𝐵 ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
90 15 88 13 89 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
91 54 56 anim12i ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
92 91 adantl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
93 92 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) )
94 53 anim1i ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑉 ) )
95 fnfvof ⊢ ( ( ( 𝐴 Fn 𝑉 ∧ 𝐵 Fn 𝑉 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) )
96 93 94 95 syl2anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) )
97 6 a1i ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ✚ = ( +g ‘ 𝑆 ) )
98 97 oveqd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑥 ) ✚ ( 𝐵 ‘ 𝑥 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) )
99 96 98 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) )
100 99 oveq1d ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
101 14 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑀 ∈ LMod )
102 101 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑀 ∈ LMod )
103 20 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ) )
104 103 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
105 35 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ) )
106 105 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
107 26 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
108 107 imp ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
109 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
110 4 fveq2i ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
111 7 1 109 29 70 110 lmodvsdir ⊢ ( ( 𝑀 ∈ LMod ∧ ( ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 ∧ ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
112 102 104 106 108 111 syl13anc ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐵 ‘ 𝑥 ) ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
113 100 112 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
114 113 mpteq2dva ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
115 114 oveq2d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
116 115 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ∘f ✚ 𝐵 ) ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
117 90 116 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) + ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
118 2 3 oveq12i ⊢ ( 𝑋 + 𝑌 ) = ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) )
119 70 oveq1i ⊢ ( 𝑅 ↑m 𝑉 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 )
120 119 eleq2i ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
121 120 biimpi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
122 121 ad2antrl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
123 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐴 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
124 101 122 53 123 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
125 119 eleq2i ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ↔ 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
126 125 biimpi ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
127 126 ad2antll ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
128 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐵 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
129 101 127 53 128 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
130 124 129 oveq12d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
131 130 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐴 ( linC ‘ 𝑀 ) 𝑉 ) + ( 𝐵 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
132 118 131 syl5eq ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) + ( 𝑀 Σg ( 𝑥 ∈ 𝑉 ↦ ( ( 𝐵 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
133 52 117 132 3eqtr4rd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑆 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑆 ) ) ) → ( 𝑋 + 𝑌 ) = ( ( 𝐴 ∘f ✚ 𝐵 ) ( linC ‘ 𝑀 ) 𝑉 ) )