Theorem dochnel

Description: A nonzero vector doesn't belong to the orthocomplement of its singleton. (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochnel.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochnel.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochnel.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochnel.v	$$⊢V={\mathrm{Base}}_U$$
	dochnel.z	$$⊢\underset{\dot{}}{0}=0_U$$
	dochnel.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochnel.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	dochnel	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochnel.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochnel.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochnel.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochnel.v	$$⊢V={\mathrm{Base}}_U$$
5		dochnel.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochnel.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		dochnel.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
8		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
9	1 3 6	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
10	7	eldifad	$$⊢\phi \to X\in V$$
11		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
12	4 8 11	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
13	9 10 12	syl2anc	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
14	4 11	lspsnid	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to X\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
15	9 10 14	syl2anc	$$⊢\phi \to X\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
16		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
17	7 16	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
18		eldifsn	$$⊢X\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\wedge X\ne \underset{\dot{}}{0}\right)$$
19	15 17 18	sylanbrc	$$⊢\phi \to X\in \left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
20	1 3 8 5 2 6 13 19	dochnel2	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)$$
21	10	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
22	1 3 2 4 11 6 21	dochocsp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
23	20 22	neleqtrd	$$⊢\phi \to \neg X\in \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$