lincellss

Description: A linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Revised by AV, 28-Jul-2019)

		Ref	Expression
	Assertion	lincellss	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to ((F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F)) \to F linC (M) V \in S)$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to M \in LMod$
2		simprl	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to F \in ({Base}_{Scalar (M)}^{V})$
3		ssexg	$⊢ (V \subseteq S \land S \in LSubSp (M)) \to V \in V$
4	3	ancoms	$⊢ (S \in LSubSp (M) \land V \subseteq S) \to V \in V$
5		eqid	$⊢ {Base}_{M} = {Base}_{M}$
6		eqid	$⊢ LSubSp (M) = LSubSp (M)$
7	5 6	lssss	$⊢ S \in LSubSp (M) \to S \subseteq {Base}_{M}$
8		sstr	$⊢ (V \subseteq S \land S \subseteq {Base}_{M}) \to V \subseteq {Base}_{M}$
9		elpwg	$⊢ V \in V \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
10	8 9	syl5ibrcom	$⊢ (V \subseteq S \land S \subseteq {Base}_{M}) \to (V \in V \to V \in 𝒫 {Base}_{M})$
11	10	expcom	$⊢ S \subseteq {Base}_{M} \to (V \subseteq S \to (V \in V \to V \in 𝒫 {Base}_{M}))$
12	7 11	syl	$⊢ S \in LSubSp (M) \to (V \subseteq S \to (V \in V \to V \in 𝒫 {Base}_{M}))$
13	12	imp	$⊢ (S \in LSubSp (M) \land V \subseteq S) \to (V \in V \to V \in 𝒫 {Base}_{M})$
14	4 13	mpd	$⊢ (S \in LSubSp (M) \land V \subseteq S) \to V \in 𝒫 {Base}_{M}$
15	14	3adant1	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to V \in 𝒫 {Base}_{M}$
16	15	adantr	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to V \in 𝒫 {Base}_{M}$
17		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)$
18	1 2 16 17	syl3anc	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
19		eqid	$⊢ Scalar (M) = Scalar (M)$
20		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
21	6 19 20	gsumlsscl	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to ((F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F)) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in S)$
22	21	imp	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) \in S$
23	18 22	eqeltrd	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land (F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F))) \to F linC (M) V \in S$
24	23	ex	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to ((F \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (F)) \to F linC (M) V \in S)$

Metamath Proof Explorer

Theorem lincellss

Proof