Theorem lincsum 44838

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.)

Hypotheses

Ref	Expression
lincsum.p	⊢ + = (+g‘𝑀)
lincsum.x	⊢ 𝑋 = (𝐴( linC ‘𝑀)𝑉)
lincsum.y	⊢ 𝑌 = (𝐵( linC ‘𝑀)𝑉)
lincsum.s	⊢ 𝑆 = (Scalar‘𝑀)
lincsum.r	⊢ 𝑅 = (Base‘𝑆)
lincsum.b	⊢ ✚ = (+g‘𝑆)

Assertion

Ref	Expression
lincsum	⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑆) ∧ 𝐵 finSupp (0g‘𝑆))) → (𝑋 + 𝑌) = ((𝐴 ∘f ✚ 𝐵)( linC ‘𝑀)𝑉))

Proof of Theorem lincsum

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  Vcvv 3441  𝒫 cpw 4497   class class class wbr 5030   ↦ cmpt 5110   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∘_f cof 7387   ↑_m cmap 8389   finSupp cfsupp 8817  Basecbs 16475  +_gcplusg 16557  Scalarcsca 16560   ·_𝑠 cvsca 16561  0_gc0g 16705   Σ_g cgsu 16706  Mndcmnd 17903  Grpcgrp 18095  CMndccmn 18898  LModclmod 19627   linC clinc 44813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-0g 16707  df-gsum 16708  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-cntz 18439  df-cmn 18900  df-abl 18901  df-mgp 19233  df-ur 19245  df-ring 19292  df-lmod 19629  df-linc 44815

This theorem is referenced by:  lincsumcl  44840