Metamath Proof Explorer

Theorem lspssp

Description: If a set of vectors is a subset of a subspace, then the span of those vectors is also contained in the subspace. (Contributed by Mario Carneiro, 4-Sep-2014)

		Ref	Expression
	Hypotheses	lspssp.s	$⊢ S = LSubSp (W)$
		lspssp.n	$⊢ N = LSpan (W)$
	Assertion	lspssp	$⊢ (W \in LMod \land U \in S \land T \subseteq U) \to N (T) \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		lspssp.s	$⊢ S = LSubSp (W)$
2		lspssp.n	$⊢ N = LSpan (W)$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
5	3 2	lspss	$⊢ (W \in LMod \land U \subseteq {Base}_{W} \land T \subseteq U) \to N (T) \subseteq N (U)$
6	4 5	syl3an2	$⊢ (W \in LMod \land U \in S \land T \subseteq U) \to N (T) \subseteq N (U)$
7	1 2	lspid	$⊢ (W \in LMod \land U \in S) \to N (U) = U$
8	7	3adant3	$⊢ (W \in LMod \land U \in S \land T \subseteq U) \to N (U) = U$
9	6 8	sseqtrd	$⊢ (W \in LMod \land U \in S \land T \subseteq U) \to N (T) \subseteq U$