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	biimpi	$⊢ F \in (S^{V}) \to F \in ({Base}_{Scalar (M)}^{V})$
11	10	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in ({Base}_{Scalar (M)}^{V})$
12	11	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})$
13		elpwg	$⊢ V \in W \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
14	1	a1i	$⊢ V \in W \to B = {Base}_{M}$
15	14	eqcomd	$⊢ V \in W \to {Base}_{M} = B$
16	15	sseq2d	$⊢ V \in W \to (V \subseteq {Base}_{M} \leftrightarrow V \subseteq B)$
17	13 16	bitr2d	$⊢ V \in W \to (V \subseteq B \leftrightarrow V \in 𝒫 {Base}_{M})$
18	17	biimpa	$⊢ (V \in W \land V \subseteq B) \to V \in 𝒫 {Base}_{M}$
19	18	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}$
20		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)$
21	5 12 19 20	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)$
22		eqid	$⊢ 0_{M} = 0_{M}$
23		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
24	23	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$
25		simpl	$⊢ (V \in W \land V \subseteq B) \to V \in W$
26	25	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$
27	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$
28		elmapi	$⊢ F \in (S^{V}) \to F : V ⟶ S$
29		ffvelrn	$⊢ (F : V ⟶ S \land v \in V) \to F (v) \in S$
30	29	ex	$⊢ F : V ⟶ S \to (v \in V \to F (v) \in S)$
31	28 30	syl	$⊢ F \in (S^{V}) \to (v \in V \to F (v) \in S)$
32	31	adantr	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to (v \in V \to F (v) \in S)$
33	32	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)$
34	33	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$
35		ssel	$⊢ V \subseteq B \to (v \in V \to v \in B)$
36	35	adantl	$⊢ (V \in W \land V \subseteq B) \to (v \in V \to v \in B)$
37	36	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)$
38	37	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$
39		eqid	$⊢ \cdot_{M} = \cdot_{M}$
40	1 2 39 3	lmodvscl	$⊢ (M \in LMod \land F (v) \in S \land v \in B) \to F (v) \cdot_{M} v \in B$
41	27 34 38 40	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$
42	41	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$
43		simpl	$⊢ (F \in (S^{V}) \land {finSupp}_{\underset{˙}{0}} (F)) \to F \in (S^{V})$
44	43	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})$
45		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)$
46	45 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)$
47	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))$
48	5 19 44 46 47	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))$
49	1 22 24 26 42 48	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$
50	21 49	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