Theorem dochsnnz

Description: The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochsnnz.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochsnnz.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochsnnz.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochsnnz.v	$$⊢V={\mathrm{Base}}_U$$
5		dochsnnz.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochsnnz.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		dochsnnz.x	$$⊢\phi \to X\in V$$
8		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
9	1 3 2 4 8 6 7	dochocsn	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)=\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
10	1 3 4 8 6 7	dvh2dim	$$⊢\phi \to \exists y\in V\neg y\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)$$
11		eleq2	$$⊢\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=V\to \left(y\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\leftrightarrow y\in V\right)$$
12	11	biimprcd	$$⊢y\in V\to \left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)=V\to y\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)$$
13	12	necon3bd	$$⊢y\in V\to \left(\neg y\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne V\right)$$
14	13	rexlimiv	$$⊢\exists y\in V\neg y\in \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne V$$
15	10 14	syl	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\ne V$$
16	9 15	eqnetrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)\ne V$$
17	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
18	1 2 3 4 5 6 17	dochn0nv	$$⊢\phi \to \left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\right)\ne V\right)$$
19	16 18	mpbird	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\ne \left\{\underset{\dot{}}{0}\right\}$$