lincfsuppcl

Description: A linear combination of vectors (with finite support) is a vector. (Contributed by AV, 25-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincfsuppcl.b	$⊢ B = {Base}_{M}$
	lincfsuppcl.r	$⊢ R = Scalar (M)$
	lincfsuppcl.s	$⊢ S = {Base}_{R}$
	lincfsuppcl.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	lincfsuppcl	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F linC (M) V \in B$

Proof

Step	Hyp	Ref	Expression
1		lincfsuppcl.b	$⊢ B = {Base}_{M}$
2		lincfsuppcl.r	$⊢ R = Scalar (M)$
3		lincfsuppcl.s	$⊢ S = {Base}_{R}$
4		lincfsuppcl.0	$⊢ \underset{˙}{0} = 0_{R}$
5		simp1	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to M \in LMod$
6	2	fveq2i	$⊢ {Base}_{R} = {Base}_{Scalar (M)}$
7	3 6	eqtri	$⊢ S = {Base}_{Scalar (M)}$
8	7	oveq1i	$⊢ S^{V} = {Base}_{Scalar (M)}^{V}$
9	8	eleq2i	$⊢ F \in (S^{V}) \leftrightarrow F \in ({Base}_{Scalar (M)}^{V})$
10	9	birani	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in ({Base}_{Scalar (M)}^{V})$
11	10	3ad2ant3	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F \in ({Base}_{Scalar (M)}^{V})$
12		elpwg	$⊢ V \in W \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
13	1	a1i	$⊢ V \in W \to B = {Base}_{M}$
14	13	eqcomd	$⊢ V \in W \to {Base}_{M} = B$
15	14	sseq2d	$⊢ V \in W \to (V \subseteq {Base}_{M} \leftrightarrow V \subseteq B)$
16	12 15	bitr2d	$⊢ V \in W \to (V \subseteq B \leftrightarrow V \in 𝒫 {Base}_{M})$
17	16	biimpa	$⊢ (V \in W \land V \subseteq B) \to V \in 𝒫 {Base}_{M}$
18	17	3ad2ant2	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to V \in 𝒫 {Base}_{M}$
19		lincval	$⊢ (M \in LMod \land F \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
20	5 11 18 19	syl3anc	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
21		eqid	$⊢ 0_{M} = 0_{M}$
22		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
23	22	3ad2ant1	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to M \in CMnd$
24		simpl	$⊢ (V \in W \land V \subseteq B) \to V \in W$
25	24	3ad2ant2	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to V \in W$
26	5	adantr	$⊢ ((M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land v \in V) \to M \in LMod$
27		elmapi	$⊢ F \in (S^{V}) \to F : V ⟶ S$
28		ffvelcdm	$⊢ (F : V ⟶ S \land v \in V) \to F (v) \in S$
29	28	ex	$⊢ F : V ⟶ S \to (v \in V \to F (v) \in S)$
30	27 29	syl	$⊢ F \in (S^{V}) \to (v \in V \to F (v) \in S)$
31	30	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to (v \in V \to F (v) \in S)$
32	31	3ad2ant3	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to (v \in V \to F (v) \in S)$
33	32	imp	$⊢ ((M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land v \in V) \to F (v) \in S$
34		ssel	$⊢ V \subseteq B \to (v \in V \to v \in B)$
35	34	adantl	$⊢ (V \in W \land V \subseteq B) \to (v \in V \to v \in B)$
36	35	3ad2ant2	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to (v \in V \to v \in B)$
37	36	imp	$⊢ ((M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land v \in V) \to v \in B$
38		eqid	$⊢ \cdot_{M} = \cdot_{M}$
39	1 2 38 3	lmodvscl	$⊢ (M \in LMod \land F (v) \in S \land v \in B) \to F (v) \cdot_{M} v \in B$
40	26 33 37 39	syl3anc	$⊢ ((M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \land v \in V) \to F (v) \cdot_{M} v \in B$
41	40	fmpttd	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to (v \in V ⟼ F (v) \cdot_{M} v) : V ⟶ B$
42		simpl	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in (S^{V})$
43	42	3ad2ant3	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F \in (S^{V})$
44		simp3r	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{\underset{˙}{0}} (F)$
45	44 4	breqtrdi	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{0_{R}} (F)$
46	2 3	scmfsupp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land F \in (S^{V}) \land {finSupp}_{0_{R}} (F)) \to {finSupp}_{0_{M}} ((v \in V ⟼ F (v) \cdot_{M} v))$
47	5 18 43 45 46	syl211anc	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{0_{M}} ((v \in V ⟼ F (v) \cdot_{M} v))$
48	1 21 23 25 41 47	gsumcl	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in B$
49	20 48	eqeltrd	$⊢ (M \in LMod \land (V \in W \land V \subseteq B) \land (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F))) \to F linC (M) V \in B$

Metamath Proof Explorer

Theorem lincfsuppcl

Proof