lincolss

Description: According to the statement in Lang p. 129, the set ( LSubSpM ) of all linear combinations of a set of vectors V is a submodule (_generated_ by V) of the module M. The elements of V are called generators of ( LSubSpM ) . (Contributed by AV, 12-Apr-2019)

		Ref	Expression
	Assertion	lincolss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo V \in LSubSp (M)$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to Scalar (M) = Scalar (M)$
2		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
3		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to {Base}_{M} = {Base}_{M}$
4		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to +_{M} = +_{M}$
5		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to \cdot_{M} = \cdot_{M}$
6		eqidd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to LSubSp (M) = LSubSp (M)$
7		eqid	$⊢ {Base}_{M} = {Base}_{M}$
8		eqid	$⊢ Scalar (M) = Scalar (M)$
9		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
10	7 8 9	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in (M LinCo V) \leftrightarrow (v \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land v = s linC (M) V)))$
11		simpl	$⊢ (v \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land v = s linC (M) V)) \to v \in {Base}_{M}$
12	10 11	syl6bi	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in (M LinCo V) \to v \in {Base}_{M})$
13	12	ssrdv	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo V \subseteq {Base}_{M}$
14		lcoel0	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to 0_{M} \in (M LinCo V)$
15	14	ne0d	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo V \neq \emptyset$
16		eqid	$⊢ \cdot_{M} = \cdot_{M}$
17		eqid	$⊢ +_{M} = +_{M}$
18	16 9 17	lincsumscmcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (x \in {Base}_{Scalar (M)} \land a \in (M LinCo V) \land b \in (M LinCo V))) \to (x \cdot_{M} a) +_{M} b \in (M LinCo V)$
19	1 2 3 4 5 6 13 15 18	islssd	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M LinCo V \in LSubSp (M)$

Metamath Proof Explorer

Theorem lincolss

Proof