Theorem lspprcl

Description: The span of a pair is a subspace (frequently used special case of lspcl ). (Contributed by NM, 11-Apr-2015)

	Ref	Expression
Hypotheses	lspval.v	$$⊢V={\mathrm{Base}}_W$$
	lspval.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspval.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspprcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspprcl.x	$$⊢\phi \to X\in V$$
	lspprcl.y	$$⊢\phi \to Y\in V$$
Assertion	lspprcl	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		lspval.v	$$⊢V={\mathrm{Base}}_W$$
2		lspval.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lspval.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspprcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspprcl.x	$$⊢\phi \to X\in V$$
6		lspprcl.y	$$⊢\phi \to Y\in V$$
7	5 6	prssd	$$⊢\phi \to \left\{X,Y\right\}\subseteq V$$
8	1 2 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X,Y\right\}\subseteq V\right)\to N\left(\left\{X,Y\right\}\right)\in S$$
9	4 7 8	syl2anc	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\in S$$