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 = ( LHyp ` K )
	dochnel.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochnel.u	|- U = ( ( DVecH ` K ) ` W )
	dochnel.v	|- V = ( Base ` U )
	dochnel.z	|- .0. = ( 0g ` U )
	dochnel.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochnel.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	dochnel	|- ( ph -> -. X e. ( ._|_ ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		dochnel.h	|- H = ( LHyp ` K )
2		dochnel.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochnel.u	|- U = ( ( DVecH ` K ) ` W )
4		dochnel.v	|- V = ( Base ` U )
5		dochnel.z	|- .0. = ( 0g ` U )
6		dochnel.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dochnel.x	|- ( ph -> X e. ( V \ { .0. } ) )
8		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
9	1 3 6	dvhlmod	|- ( ph -> U e. LMod )
10	7	eldifad	|- ( ph -> X e. V )
11		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
12	4 8 11	lspsncl	|- ( ( U e. LMod /\ X e. V ) -> ( ( LSpan ` U ) ` { X } ) e. ( LSubSp ` U ) )
13	9 10 12	syl2anc	|- ( ph -> ( ( LSpan ` U ) ` { X } ) e. ( LSubSp ` U ) )
14	4 11	lspsnid	|- ( ( U e. LMod /\ X e. V ) -> X e. ( ( LSpan ` U ) ` { X } ) )
15	9 10 14	syl2anc	|- ( ph -> X e. ( ( LSpan ` U ) ` { X } ) )
16		eldifsni	|- ( X e. ( V \ { .0. } ) -> X =/= .0. )
17	7 16	syl	|- ( ph -> X =/= .0. )
18		eldifsn	|- ( X e. ( ( ( LSpan ` U ) ` { X } ) \ { .0. } ) <-> ( X e. ( ( LSpan ` U ) ` { X } ) /\ X =/= .0. ) )
19	15 17 18	sylanbrc	|- ( ph -> X e. ( ( ( LSpan ` U ) ` { X } ) \ { .0. } ) )
20	1 3 8 5 2 6 13 19	dochnel2	|- ( ph -> -. X e. ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) )
21	10	snssd	|- ( ph -> { X } C_ V )
22	1 3 2 4 11 6 21	dochocsp	|- ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
23	20 22	neleqtrd	|- ( ph -> -. X e. ( ._|_ ` { X } ) )