Theorem dochsnshp

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

	Ref	Expression
Hypotheses	dochsnshp.h	|- H = ( LHyp ` K )
	dochsnshp.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochsnshp.u	|- U = ( ( DVecH ` K ) ` W )
	dochsnshp.v	|- V = ( Base ` U )
	dochsnshp.z	|- .0. = ( 0g ` U )
	dochsnshp.y	|- Y = ( LSHyp ` U )
	dochsnshp.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochsnshp.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	dochsnshp	|- ( ph -> ( ._|_ ` { X } ) e. Y )

Proof

Step	Hyp	Ref	Expression
1		dochsnshp.h	|- H = ( LHyp ` K )
2		dochsnshp.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochsnshp.u	|- U = ( ( DVecH ` K ) ` W )
4		dochsnshp.v	|- V = ( Base ` U )
5		dochsnshp.z	|- .0. = ( 0g ` U )
6		dochsnshp.y	|- Y = ( LSHyp ` U )
7		dochsnshp.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		dochsnshp.x	|- ( ph -> X e. ( V \ { .0. } ) )
9		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
10	8	eldifad	|- ( ph -> X e. V )
11	10	snssd	|- ( ph -> { X } C_ V )
12	1 3 2 4 9 7 11	dochocsp	|- ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
13		eqid	|- ( LSAtoms ` U ) = ( LSAtoms ` U )
14	1 3 7	dvhlmod	|- ( ph -> U e. LMod )
15	4 9 5 13 14 8	lsatlspsn	|- ( ph -> ( ( LSpan ` U ) ` { X } ) e. ( LSAtoms ` U ) )
16	1 3 2 13 6 7 15	dochsatshp	|- ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) e. Y )
17	12 16	eqeltrrd	|- ( ph -> ( ._|_ ` { X } ) e. Y )