Theorem lsptpcl

Description: The span of an unordered triple is a subspace (frequently used special case of lspcl ). (Contributed by NM, 22-May-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$$
	lsptpcl.z	$$⊢\phi \to Z\in V$$
Assertion	lsptpcl	$$⊢\phi \to N\left(\left\{X,Y,Z\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		lsptpcl.z	$$⊢\phi \to Z\in V$$
8		df-tp	$$⊢\left\{X,Y,Z\right\}=\left\{X,Y\right\}\cup \left\{Z\right\}$$
9	5 6	prssd	$$⊢\phi \to \left\{X,Y\right\}\subseteq V$$
10	7	snssd	$$⊢\phi \to \left\{Z\right\}\subseteq V$$
11	9 10	unssd	$$⊢\phi \to \left\{X,Y\right\}\cup \left\{Z\right\}\subseteq V$$
12	8 11	eqsstrid	$$⊢\phi \to \left\{X,Y,Z\right\}\subseteq V$$
13	1 2 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X,Y,Z\right\}\subseteq V\right)\to N\left(\left\{X,Y,Z\right\}\right)\in S$$
14	4 12 13	syl2anc	$$⊢\phi \to N\left(\left\{X,Y,Z\right\}\right)\in S$$