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

Metamath Proof Explorer

Theorem ellspsn3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn3 analog.) (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	lspsnss.s	$⊢ S = LSubSp (W)$
	lspsnss.n	$⊢ N = LSpan (W)$
	ellspsn3.w	$⊢ φ \to W \in LMod$
	ellspsn3.u	$⊢ φ \to U \in S$
	ellspsn3.x	$⊢ φ \to X \in U$
	ellspsn3.y	$⊢ φ \to Y \in N (\{X\})$
Assertion	ellspsn3	$⊢ φ \to Y \in U$

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	$⊢ S = LSubSp (W)$
2		lspsnss.n	$⊢ N = LSpan (W)$
3		ellspsn3.w	$⊢ φ \to W \in LMod$
4		ellspsn3.u	$⊢ φ \to U \in S$
5		ellspsn3.x	$⊢ φ \to X \in U$
6		ellspsn3.y	$⊢ φ \to Y \in N (\{X\})$
7	1 2	lspsnss	$⊢ (W \in LMod \land U \in S \land X \in U) \to N (\{X\}) \subseteq U$
8	3 4 5 7	syl3anc	$⊢ φ \to N (\{X\}) \subseteq U$
9	8 6	sseldd	$⊢ φ \to Y \in U$