Theorem lspsnsubn0

Description: Unequal singleton spans imply nonzero vector subtraction. (Contributed by NM, 19-Mar-2015)

	Ref	Expression
Hypotheses	lspsnsubn0.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnsubn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsnsubn0.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	lspsnsubn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspsnsubn0.x	$$⊢\phi \to X\in V$$
	lspsnsubn0.y	$$⊢\phi \to Y\in V$$
	lspsnsubn0.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
Assertion	lspsnsubn0	$$⊢\phi \to X\underset{\dot{}}{-}Y\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lspsnsubn0.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnsubn0.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspsnsubn0.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		lspsnsubn0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lspsnsubn0.x	$$⊢\phi \to X\in V$$
6		lspsnsubn0.y	$$⊢\phi \to Y\in V$$
7		lspsnsubn0.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
8	1 2 3	lmodsubeq0	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to \left(X\underset{\dot{}}{-}Y=\underset{\dot{}}{0}\leftrightarrow X=Y\right)$$
9	4 5 6 8	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y=\underset{\dot{}}{0}\leftrightarrow X=Y\right)$$
10		sneq	$$⊢X=Y\to \left\{X\right\}=\left\{Y\right\}$$
11	10	fveq2d	$$⊢X=Y\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$
12	9 11	biimtrdi	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y=\underset{\dot{}}{0}\to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\right)$$
13	12	necon3d	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\to X\underset{\dot{}}{-}Y\ne \underset{\dot{}}{0}\right)$$
14	7 13	mpd	$$⊢\phi \to X\underset{\dot{}}{-}Y\ne \underset{\dot{}}{0}$$