Theorem lspindp4

Description: (Partial) independence of 3 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspindp3.v	$$⊢V={\mathrm{Base}}_W$$
2		lspindp3.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lspindp4.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspindp4.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspindp4.x	$$⊢\phi \to X\in V$$
6		lspindp4.y	$$⊢\phi \to Y\in V$$
7		lspindp4.z	$$⊢\phi \to Z\in V$$
8		lspindp4.e	$$⊢\phi \to \neg Z\in N\left(\left\{X,Y\right\}\right)$$
9	1 2 3 4 5 6	lspprabs	$$⊢\phi \to N\left(\left\{X,X\underset{\dot{}}{+}Y\right\}\right)=N\left(\left\{X,Y\right\}\right)$$
10	8 9	neleqtrrd	$$⊢\phi \to \neg Z\in N\left(\left\{X,X\underset{\dot{}}{+}Y\right\}\right)$$