This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspssid

Description: A set of vectors is a subset of its span. ( spanss2 analog.) (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspss.v	$⊢ V = {Base}_{W}$
	lspss.n	$⊢ N = LSpan (W)$
Assertion	lspssid	$⊢ (W \in LMod \land U \subseteq V) \to U \subseteq N (U)$

Proof

Step	Hyp	Ref	Expression
1		lspss.v	$⊢ V = {Base}_{W}$
2		lspss.n	$⊢ N = LSpan (W)$
3		ssintub	$⊢ U \subseteq ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
4		eqid	$⊢ LSubSp (W) = LSubSp (W)$
5	1 4 2	lspval	$⊢ (W \in LMod \land U \subseteq V) \to N (U) = ⋂ \{t \in LSubSp (W) \| U \subseteq t\}$
6	3 5	sseqtrrid	$⊢ (W \in LMod \land U \subseteq V) \to U \subseteq N (U)$