Theorem lspprvacl

Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspprvacl.v	$$⊢V={\mathrm{Base}}_W$$
	lspprvacl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lspprvacl.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspprvacl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspprvacl.x	$$⊢\phi \to X\in V$$
	lspprvacl.y	$$⊢\phi \to Y\in V$$
Assertion	lspprvacl	$$⊢\phi \to X\underset{\dot{}}{+}Y\in N\left(\left\{X,Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspprvacl.v	$$⊢V={\mathrm{Base}}_W$$
2		lspprvacl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lspprvacl.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspprvacl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspprvacl.x	$$⊢\phi \to X\in V$$
6		lspprvacl.y	$$⊢\phi \to Y\in V$$
7		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
8	1 7 3 4 5 6	lspprcl	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
9	1 3 4 5 6	lspprid1	$$⊢\phi \to X\in N\left(\left\{X,Y\right\}\right)$$
10	1 3 4 5 6	lspprid2	$$⊢\phi \to Y\in N\left(\left\{X,Y\right\}\right)$$
11	2 7	lssvacl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge N\left(\left\{X,Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)\right)\wedge \left(X\in N\left(\left\{X,Y\right\}\right)\wedge Y\in N\left(\left\{X,Y\right\}\right)\right)\right)\to X\underset{\dot{}}{+}Y\in N\left(\left\{X,Y\right\}\right)$$
12	4 8 9 10 11	syl22anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in N\left(\left\{X,Y\right\}\right)$$