Theorem dochsnnz

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

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

Proof

Step	Hyp	Ref	Expression
1		dochsnnz.h	|- H = ( LHyp ` K )
2		dochsnnz.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochsnnz.u	|- U = ( ( DVecH ` K ) ` W )
4		dochsnnz.v	|- V = ( Base ` U )
5		dochsnnz.z	|- .0. = ( 0g ` U )
6		dochsnnz.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dochsnnz.x	|- ( ph -> X e. V )
8		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
9	1 3 2 4 8 6 7	dochocsn	|- ( ph -> ( ._|_ ` ( ._|_ ` { X } ) ) = ( ( LSpan ` U ) ` { X } ) )
10	1 3 4 8 6 7	dvh2dim	|- ( ph -> E. y e. V -. y e. ( ( LSpan ` U ) ` { X } ) )
11		eleq2	|- ( ( ( LSpan ` U ) ` { X } ) = V -> ( y e. ( ( LSpan ` U ) ` { X } ) <-> y e. V ) )
12	11	biimprcd	|- ( y e. V -> ( ( ( LSpan ` U ) ` { X } ) = V -> y e. ( ( LSpan ` U ) ` { X } ) ) )
13	12	necon3bd	|- ( y e. V -> ( -. y e. ( ( LSpan ` U ) ` { X } ) -> ( ( LSpan ` U ) ` { X } ) =/= V ) )
14	13	rexlimiv	|- ( E. y e. V -. y e. ( ( LSpan ` U ) ` { X } ) -> ( ( LSpan ` U ) ` { X } ) =/= V )
15	10 14	syl	|- ( ph -> ( ( LSpan ` U ) ` { X } ) =/= V )
16	9 15	eqnetrd	|- ( ph -> ( ._|_ ` ( ._|_ ` { X } ) ) =/= V )
17	7	snssd	|- ( ph -> { X } C_ V )
18	1 2 3 4 5 6 17	dochn0nv	|- ( ph -> ( ( ._|_ ` { X } ) =/= { .0. } <-> ( ._|_ ` ( ._|_ ` { X } ) ) =/= V ) )
19	16 18	mpbird	|- ( ph -> ( ._|_ ` { X } ) =/= { .0. } )