ellcoellss

Description: Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	ellcoellss	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to \forall x \in (M LinCo V) x \in S$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to M \in LMod$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ LSubSp (M) = LSubSp (M)$
4	2 3	lssss	$⊢ S \in LSubSp (M) \to S \subseteq {Base}_{M}$
5	4	3ad2ant2	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to S \subseteq {Base}_{M}$
6		sstr	$⊢ (V \subseteq S \land S \subseteq {Base}_{M}) \to V \subseteq {Base}_{M}$
7		fvex	$⊢ {Base}_{M} \in V$
8	7	ssex	$⊢ V \subseteq {Base}_{M} \to V \in V$
9		elpwg	$⊢ V \in V \to (V \in 𝒫 {Base}_{M} \leftrightarrow V \subseteq {Base}_{M})$
10	9	biimprd	$⊢ V \in V \to (V \subseteq {Base}_{M} \to V \in 𝒫 {Base}_{M})$
11	8 10	mpcom	$⊢ V \subseteq {Base}_{M} \to V \in 𝒫 {Base}_{M}$
12	6 11	syl	$⊢ (V \subseteq S \land S \subseteq {Base}_{M}) \to V \in 𝒫 {Base}_{M}$
13	12	ex	$⊢ V \subseteq S \to (S \subseteq {Base}_{M} \to V \in 𝒫 {Base}_{M})$
14	13	3ad2ant3	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to (S \subseteq {Base}_{M} \to V \in 𝒫 {Base}_{M})$
15	5 14	mpd	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to V \in 𝒫 {Base}_{M}$
16		eqid	$⊢ Scalar (M) = Scalar (M)$
17		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
18	2 16 17	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (x \in (M LinCo V) \leftrightarrow (x \in {Base}_{M} \land \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V)))$
19	1 15 18	syl2anc	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to (x \in (M LinCo V) \leftrightarrow (x \in {Base}_{M} \land \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V)))$
20		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)$
21	20	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 f linC (M) V \in S$
22		eleq1	$⊢ x = f linC (M) V \to (x \in S \leftrightarrow f linC (M) V \in S)$
23	21 22	imbitrrid	$⊢ x = f linC (M) V \to (((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 x \in S)$
24	23	expd	$⊢ x = f linC (M) V \to ((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 x \in S))$
25	24	com12	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to (x = f linC (M) V \to ((f \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (f)) \to x \in S))$
26	25	adantr	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land x \in {Base}_{M}) \to (x = f linC (M) V \to ((f \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (f)) \to x \in S))$
27	26	com13	$⊢ (f \in ({Base}_{Scalar (M)}^{V}) \land {finSupp}_{0_{Scalar (M)}} (f)) \to (x = f linC (M) V \to (((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land x \in {Base}_{M}) \to x \in S))$
28	27	impr	$⊢ (f \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V)) \to (((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land x \in {Base}_{M}) \to x \in S)$
29	28	rexlimiva	$⊢ \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V) \to (((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land x \in {Base}_{M}) \to x \in S)$
30	29	com12	$⊢ ((M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \land x \in {Base}_{M}) \to (\exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V) \to x \in S)$
31	30	expimpd	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to ((x \in {Base}_{M} \land \exists f \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (f) \land x = f linC (M) V)) \to x \in S)$
32	19 31	sylbid	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to (x \in (M LinCo V) \to x \in S)$
33	32	ralrimiv	$⊢ (M \in LMod \land S \in LSubSp (M) \land V \subseteq S) \to \forall x \in (M LinCo V) x \in S$

Metamath Proof Explorer

Theorem ellcoellss

Proof