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	$⊢ \underset{˙}{+} = +_{M}$
	lincsum.x	$⊢ X = A linC (M) V$
	lincsum.y	$⊢ Y = B linC (M) V$
	lincsum.s	$⊢ S = Scalar (M)$
	lincsum.r	$⊢ R = {Base}_{S}$
	lincsum.b	$⊢ \underset{˙}{✚} = +_{S}$
Assertion	lincsum	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land B \in (R^{V})) \land ({finSupp}_{0_{S}} (A) \land {finSupp}_{0_{S}} (B))) \to X \underset{˙}{+} Y = (A {\underset{˙}{✚}}_{f} B) linC (M) V$

Proof

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

Metamath Proof Explorer

Theorem lincsum

Proof