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		grpmnd	$⊢ S \in Grp \to S \in Mnd$
62	60 61	syl	$⊢ M \in LMod \to S \in Mnd$
63	62	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$
64		ffvelrn	$⊢ (A : V ⟶ R \land y \in V) \to A (y) \in R$
65	64	ex	$⊢ A : V ⟶ R \to (y \in V \to A (y) \in R)$
66	17 65	syl	$⊢ A \in (R^{V}) \to (y \in V \to A (y) \in R)$
67	66	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)$
68	67	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$
69	4	fveq2i	$⊢ {Base}_{S} = {Base}_{Scalar (M)}$
70	5 69	eqtri	$⊢ R = {Base}_{Scalar (M)}$
71	68 70	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)}$
72		ffvelrn	$⊢ (B : V ⟶ R \land y \in V) \to B (y) \in R$
73	72 70	eleqtrdi	$⊢ (B : V ⟶ R \land y \in V) \to B (y) \in {Base}_{Scalar (M)}$
74	73	ex	$⊢ B : V ⟶ R \to (y \in V \to B (y) \in {Base}_{Scalar (M)})$
75	32 74	syl	$⊢ B \in (R^{V}) \to (y \in V \to B (y) \in {Base}_{Scalar (M)})$
76	75	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)})$
77	76	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)}$
78	4	eqcomi	$⊢ Scalar (M) = S$
79	78	fveq2i	$⊢ {Base}_{Scalar (M)} = {Base}_{S}$
80	79 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)}$
81	63 71 77 80	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)}$
82	81	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)}$
83		fvex	$⊢ {Base}_{Scalar (M)} \in V$
84		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)})$
85	83 53 84	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)})$
86	82 85	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})$
87	86	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})$
88	59 87	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})$
89		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)$
90	15 88 13 89	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)$
91	54 56	anim12i	$⊢ (A \in (R^{V}) \land B \in (R^{V})) \to (A Fn V \land B Fn V)$
92	91	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)$
93	92	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)$
94	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)$
95		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)$
96	93 94 95	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)$
97	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}$
98	97	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)$
99	96 98	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)$
100	99	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$
101	14	adantr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land B \in (R^{V}))) \to M \in LMod$
102	101	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$
103	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)$
104	103	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$
105	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)$
106	105	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$
107	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})$
108	107	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}$
109		eqid	$⊢ Scalar (M) = Scalar (M)$
110	4	fveq2i	$⊢ +_{S} = +_{Scalar (M)}$
111	7 1 109 29 70 110	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)$
112	102 104 106 108 111	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)$
113	100 112	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)$
114	113	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))$
115	114	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))$
116	115	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))$
117	90 116	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))$
118	2 3	oveq12i	$⊢ X \underset{˙}{+} Y = (A linC (M) V) \underset{˙}{+} (B linC (M) V)$
119	70	oveq1i	$⊢ R^{V} = {Base}_{Scalar (M)}^{V}$
120	119	eleq2i	$⊢ A \in (R^{V}) \leftrightarrow A \in ({Base}_{Scalar (M)}^{V})$
121	120	biimpi	$⊢ A \in (R^{V}) \to A \in ({Base}_{Scalar (M)}^{V})$
122	121	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})$
123		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)$
124	101 122 53 123	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)$
125	119	eleq2i	$⊢ B \in (R^{V}) \leftrightarrow B \in ({Base}_{Scalar (M)}^{V})$
126	125	biimpi	$⊢ B \in (R^{V}) \to B \in ({Base}_{Scalar (M)}^{V})$
127	126	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})$
128		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)$
129	101 127 53 128	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)$
130	124 129	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))$
131	130	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))$
132	118 131	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))$
133	52 117 132	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