Theorem lspdisjb

Description: A nonzero vector is not in a subspace iff its span is disjoint with the subspace. (Contributed by NM, 23-Apr-2015)

	Ref	Expression
Hypotheses	lspdisjb.v	$$⊢V={\mathrm{Base}}_W$$
	lspdisjb.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lspdisjb.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspdisjb.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspdisjb.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspdisjb.u	$$⊢\phi \to U\in S$$
	lspdisjb.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	lspdisjb	$$⊢\phi \to \left(\neg X\in U\leftrightarrow N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspdisjb.v	$$⊢V={\mathrm{Base}}_W$$
2		lspdisjb.o	$$⊢\underset{\dot{}}{0}=0_W$$
3		lspdisjb.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspdisjb.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
5		lspdisjb.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lspdisjb.u	$$⊢\phi \to U\in S$$
7		lspdisjb.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
8	5	adantr	$$⊢\left(\phi \wedge \neg X\in U\right)\to W\in \mathrm{LVec}$$
9	6	adantr	$$⊢\left(\phi \wedge \neg X\in U\right)\to U\in S$$
10	7	eldifad	$$⊢\phi \to X\in V$$
11	10	adantr	$$⊢\left(\phi \wedge \neg X\in U\right)\to X\in V$$
12		simpr	$$⊢\left(\phi \wedge \neg X\in U\right)\to \neg X\in U$$
13	1 2 3 4 8 9 11 12	lspdisj	$$⊢\left(\phi \wedge \neg X\in U\right)\to N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}$$
14		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
15	7 14	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
16	15	adantr	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
17		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
18	5 17	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
19	1 3	lspsnid	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to X\in N\left(\left\{X\right\}\right)$$
20	18 10 19	syl2anc	$$⊢\phi \to X\in N\left(\left\{X\right\}\right)$$
21		elin	$$⊢X\in \left(N\left(\left\{X\right\}\right)\cap U\right)\leftrightarrow \left(X\in N\left(\left\{X\right\}\right)\wedge X\in U\right)$$
22		eleq2	$$⊢N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\to \left(X\in \left(N\left(\left\{X\right\}\right)\cap U\right)\leftrightarrow X\in \left\{\underset{\dot{}}{0}\right\}\right)$$
23		elsni	$$⊢X\in \left\{\underset{\dot{}}{0}\right\}\to X=\underset{\dot{}}{0}$$
24	22 23	syl6bi	$$⊢N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\to \left(X\in \left(N\left(\left\{X\right\}\right)\cap U\right)\to X=\underset{\dot{}}{0}\right)$$
25	21 24	syl5bir	$$⊢N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\to \left(\left(X\in N\left(\left\{X\right\}\right)\wedge X\in U\right)\to X=\underset{\dot{}}{0}\right)$$
26	25	expd	$$⊢N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\to \left(X\in N\left(\left\{X\right\}\right)\to \left(X\in U\to X=\underset{\dot{}}{0}\right)\right)$$
27	20 26	mpan9	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)\to \left(X\in U\to X=\underset{\dot{}}{0}\right)$$
28	27	necon3ad	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)\to \left(X\ne \underset{\dot{}}{0}\to \neg X\in U\right)$$
29	16 28	mpd	$$⊢\left(\phi \wedge N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)\to \neg X\in U$$
30	13 29	impbida	$$⊢\phi \to \left(\neg X\in U\leftrightarrow N\left(\left\{X\right\}\right)\cap U=\left\{\underset{\dot{}}{0}\right\}\right)$$