Theorem dochsnshp

Description: The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochsnshp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochsnshp.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochsnshp.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochsnshp.v	$$⊢V={\mathrm{Base}}_U$$
5		dochsnshp.z	$$⊢\underset{\dot{}}{0}=0_U$$
6		dochsnshp.y	$$⊢Y=\mathrm{LSHyp}\left(U\right)$$
7		dochsnshp.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		dochsnshp.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
10	8	eldifad	$$⊢\phi \to X\in V$$
11	10	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
12	1 3 2 4 9 7 11	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)$$
13		eqid	$$⊢\mathrm{LSAtoms}\left(U\right)=\mathrm{LSAtoms}\left(U\right)$$
14	1 3 7	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
15	4 9 5 13 14 8	lsatlspsn	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\in \mathrm{LSAtoms}\left(U\right)$$
16	1 3 2 13 6 7 15	dochsatshp	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(U\right)\left(\left\{X\right\}\right)\right)\in Y$$
17	12 16	eqeltrrd	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{X\right\}\right)\in Y$$