linccl

Description: A linear combination of vectors is a vector. (Contributed by AV, 31-Mar-2019)

	Ref	Expression
Hypotheses	linccl.b	$⊢ B = {Base}_{M}$
	linccl.r	$⊢ R = {Base}_{Scalar (M)}$
Assertion	linccl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S linC (M) V \in B$

Proof

Step	Hyp	Ref	Expression
1		linccl.b	$⊢ B = {Base}_{M}$
2		linccl.r	$⊢ R = {Base}_{Scalar (M)}$
3		simpl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to M \in LMod$
4	2	oveq1i	$⊢ R^{V} = {Base}_{Scalar (M)}^{V}$
5	4	eleq2i	$⊢ S \in (R^{V}) \leftrightarrow S \in ({Base}_{Scalar (M)}^{V})$
6	5	biimpi	$⊢ S \in (R^{V}) \to S \in ({Base}_{Scalar (M)}^{V})$
7	6	3ad2ant3	$⊢ (V \in Fin \land V \subseteq B \land S \in (R^{V})) \to S \in ({Base}_{Scalar (M)}^{V})$
8	7	adantl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S \in ({Base}_{Scalar (M)}^{V})$
9	1	sseq2i	$⊢ V \subseteq B \leftrightarrow V \subseteq {Base}_{M}$
10		fvex	$⊢ {Base}_{M} \in V$
11	10	ssex	$⊢ V \subseteq {Base}_{M} \to V \in V$
12		elpwg	$⊢ V \in V \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
13	11 12	syl	$⊢ V \subseteq {Base}_{M} \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
14	13	ibir	$⊢ V \subseteq {Base}_{M} \to V \in 𝒫 {Base}_{M}$
15	9 14	sylbi	$⊢ V \subseteq B \to V \in 𝒫 {Base}_{M}$
16	15	3ad2ant2	$⊢ (V \in Fin \land V \subseteq B \land S \in (R^{V})) \to V \in 𝒫 {Base}_{M}$
17	16	adantl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to V \in 𝒫 {Base}_{M}$
18		lincval	$⊢ (M \in LMod \land S \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to S linC (M) V = \underset{v \in V}{\sum_{M}} (S (v) \cdot_{M} v)$
19	3 8 17 18	syl3anc	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S linC (M) V = \underset{v \in V}{\sum_{M}} (S (v) \cdot_{M} v)$
20		eqid	$⊢ 0_{M} = 0_{M}$
21		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
22	21	adantr	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to M \in CMnd$
23		simpr1	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to V \in Fin$
24	3	adantr	$⊢ ((M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \land v \in V) \to M \in LMod$
25	2	fvexi	$⊢ R \in V$
26		elmapg	$⊢ (R \in V \land V \in Fin) \to (S \in (R^{V}) \leftrightarrow S : V ⟶ R)$
27	25 26	mpan	$⊢ V \in Fin \to (S \in (R^{V}) \leftrightarrow S : V ⟶ R)$
28		ffvelcdm	$⊢ (S : V ⟶ R \land v \in V) \to S (v) \in R$
29	28	ex	$⊢ S : V ⟶ R \to (v \in V \to S (v) \in R)$
30	27 29	syl6bi	$⊢ V \in Fin \to (S \in (R^{V}) \to (v \in V \to S (v) \in R))$
31	30	imp	$⊢ (V \in Fin \land S \in (R^{V})) \to (v \in V \to S (v) \in R)$
32	31	3adant2	$⊢ (V \in Fin \land V \subseteq B \land S \in (R^{V})) \to (v \in V \to S (v) \in R)$
33	32	adantl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to (v \in V \to S (v) \in R)$
34	33	imp	$⊢ ((M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \land v \in V) \to S (v) \in R$
35		ssel	$⊢ V \subseteq B \to (v \in V \to v \in B)$
36	35	3ad2ant2	$⊢ (V \in Fin \land V \subseteq B \land S \in (R^{V})) \to (v \in V \to v \in B)$
37	36	adantl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to (v \in V \to v \in B)$
38	37	imp	$⊢ ((M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \land v \in V) \to v \in B$
39		eqid	$⊢ Scalar (M) = Scalar (M)$
40		eqid	$⊢ \cdot_{M} = \cdot_{M}$
41	1 39 40 2	lmodvscl	$⊢ (M \in LMod \land S (v) \in R \land v \in B) \to S (v) \cdot_{M} v \in B$
42	24 34 38 41	syl3anc	$⊢ ((M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \land v \in V) \to S (v) \cdot_{M} v \in B$
43	42	fmpttd	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to (v \in V ⟼ S (v) \cdot_{M} v) : V ⟶ B$
44	16	anim2i	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
45		simpr3	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S \in (R^{V})$
46		elmapi	$⊢ S \in (R^{V}) \to S : V ⟶ R$
47	46	3ad2ant3	$⊢ (V \in Fin \land V \subseteq B \land S \in (R^{V})) \to S : V ⟶ R$
48	47	adantl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S : V ⟶ R$
49		fvexd	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to 0_{Scalar (M)} \in V$
50	48 23 49	fdmfifsupp	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to {finSupp}_{0_{Scalar (M)}} (S)$
51	39 2	scmfsupp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land S \in (R^{V}) \land {finSupp}_{0_{Scalar (M)}} (S)) \to {finSupp}_{0_{M}} ((v \in V ⟼ S (v) \cdot_{M} v))$
52	44 45 50 51	syl3anc	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to {finSupp}_{0_{M}} ((v \in V ⟼ S (v) \cdot_{M} v))$
53	1 20 22 23 43 52	gsumcl	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to \underset{v \in V}{\sum_{M}} (S (v) \cdot_{M} v) \in B$
54	19 53	eqeltrd	$⊢ (M \in LMod \land (V \in Fin \land V \subseteq B \land S \in (R^{V}))) \to S linC (M) V \in B$

Metamath Proof Explorer

Theorem linccl

Proof