Theorem lspindp3

Description: Independence of 2 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$$
	lspindp3.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspindp3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspindp3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspindp3.x	$$⊢\phi \to X\in V$$
	lspindp3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lspindp3.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
Assertion	lspindp3	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{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		lspindp3.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		lspindp3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
5		lspindp3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lspindp3.x	$$⊢\phi \to X\in V$$
7		lspindp3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
8		lspindp3.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
9	5	adantr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to W\in \mathrm{LVec}$$
10	6	adantr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to X\in V$$
11	7	adantr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		simpr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
13	1 2 3 4 9 10 11 12	lspabs2	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
14	13	ex	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\right)$$
15	14	necon3d	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)\right)$$
16	8 15	mpd	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$