Theorem lspsnne2

Description: Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015)

	Ref	Expression
Hypotheses	lspsnne2.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnne2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspsnne2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lspsnne2.x	$$⊢\phi \to X\in V$$
	lspsnne2.y	$$⊢\phi \to Y\in V$$
	lspsnne2.e	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$
Assertion	lspsnne2	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsnne2.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnne2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lspsnne2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lspsnne2.x	$$⊢\phi \to X\in V$$
5		lspsnne2.y	$$⊢\phi \to Y\in V$$
6		lspsnne2.e	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$
7		eqimss	$$⊢N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\to N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)$$
8		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
9	1 8 2	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
10	3 5 9	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
11	1 8 2 3 10 4	ellspsn5b	$$⊢\phi \to \left(X\in N\left(\left\{Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\right)$$
12	7 11	imbitrrid	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\to X\in N\left(\left\{Y\right\}\right)\right)$$
13	12	necon3bd	$$⊢\phi \to \left(\neg X\in N\left(\left\{Y\right\}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
14	6 13	mpd	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$