Theorem lspsnne1

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

	Ref	Expression
Hypotheses	lspsnne1.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnne1.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspsnne1.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspsnne1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspsnne1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lspsnne1.y	$$⊢\phi \to Y\in V$$
	lspsnne1.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
Assertion	lspsnne1	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsnne1.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnne1.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspsnne1.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspsnne1.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lspsnne1.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
6		lspsnne1.y	$$⊢\phi \to Y\in V$$
7		lspsnne1.e	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
8		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
9		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
10	4 9	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
11	1 8 3	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
12	10 6 11	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
13	5	eldifad	$$⊢\phi \to X\in V$$
14	1 8 3 10 12 13	lspsnel5	$$⊢\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)$$
15	14	notbid	$$⊢\phi \to \left(\neg X\in N\left(\left\{Y\right\}\right)\leftrightarrow \neg N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\right)$$
16	1 2 3 4 5 6	lspsncmp	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\right)$$
17	16	necon3bbid	$$⊢\phi \to \left(\neg N\left(\left\{X\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
18	15 17	bitrd	$$⊢\phi \to \left(\neg X\in N\left(\left\{Y\right\}\right)\leftrightarrow N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
19	7 18	mpbird	$$⊢\phi \to \neg X\in N\left(\left\{Y\right\}\right)$$