lspprid1

Description: A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015)

Step	Hyp	Ref	Expression
1		lspprid.v	$⊢ V = {Base}_{W}$
2		lspprid.n	$⊢ N = LSpan (W)$
3		lspprid.w	$⊢ φ \to W \in LMod$
4		lspprid.x	$⊢ φ \to X \in V$
5		lspprid.y	$⊢ φ \to Y \in V$
6	4 5	prssd	$⊢ φ \to \{X, Y\} \subseteq V$
7		snsspr1	$⊢ \{X\} \subseteq \{X, Y\}$
8	7	a1i	$⊢ φ \to \{X\} \subseteq \{X, Y\}$
9	1 2	lspss	$⊢ (W \in LMod \land \{X, Y\} \subseteq V \land \{X\} \subseteq \{X, Y\}) \to N (\{X\}) \subseteq N (\{X, Y\})$
10	3 6 8 9	syl3anc	$⊢ φ \to N (\{X\}) \subseteq N (\{X, Y\})$
11		eqid	$⊢ LSubSp (W) = LSubSp (W)$
12	1 11 2 3 4 5	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (W)$
13	1 11 2 3 12 4	ellspsn5b	$⊢ φ \to (X \in N (\{X, Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{X, Y\}))$
14	10 13	mpbird	$⊢ φ \to X \in N (\{X, Y\})$

Metamath Proof Explorer