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		ffvelcdm	⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝑅 )
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		ffvelcdm	⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝑅 )
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		ffvelcdm	⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑅 )
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		ffvelcdm	⊢ ( ( 𝐵 : 𝑉 ⟶ 𝑅 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑦 ) ∈ 𝑅 )
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	eqtrid	⊢ ( ( ( 𝑀 ∈ 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 ‘ 𝑀 ) 𝑉 ) )