Theorem dochnel2

Description: A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015)

	Ref	Expression
Hypotheses	dochnoncon.h	|- H = ( LHyp ` K )
	dochnoncon.u	|- U = ( ( DVecH ` K ) ` W )
	dochnoncon.s	|- S = ( LSubSp ` U )
	dochnoncon.z	|- .0. = ( 0g ` U )
	dochnoncon.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochnel2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochnel2.t	|- ( ph -> T e. S )
	dochnel2.x	|- ( ph -> X e. ( T \ { .0. } ) )
Assertion	dochnel2	|- ( ph -> -. X e. ( ._|_ ` T ) )

Proof

Step	Hyp	Ref	Expression
1		dochnoncon.h	|- H = ( LHyp ` K )
2		dochnoncon.u	|- U = ( ( DVecH ` K ) ` W )
3		dochnoncon.s	|- S = ( LSubSp ` U )
4		dochnoncon.z	|- .0. = ( 0g ` U )
5		dochnoncon.o	|- ._|_ = ( ( ocH ` K ) ` W )
6		dochnel2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dochnel2.t	|- ( ph -> T e. S )
8		dochnel2.x	|- ( ph -> X e. ( T \ { .0. } ) )
9	8	eldifbd	|- ( ph -> -. X e. { .0. } )
10	8	eldifad	|- ( ph -> X e. T )
11		elin	|- ( X e. ( T i^i ( ._|_ ` T ) ) <-> ( X e. T /\ X e. ( ._|_ ` T ) ) )
12	1 2 3 4 5	dochnoncon	|- ( ( ( K e. HL /\ W e. H ) /\ T e. S ) -> ( T i^i ( ._|_ ` T ) ) = { .0. } )
13	6 7 12	syl2anc	|- ( ph -> ( T i^i ( ._|_ ` T ) ) = { .0. } )
14	13	eleq2d	|- ( ph -> ( X e. ( T i^i ( ._|_ ` T ) ) <-> X e. { .0. } ) )
15	11 14	bitr3id	|- ( ph -> ( ( X e. T /\ X e. ( ._|_ ` T ) ) <-> X e. { .0. } ) )
16	15	biimpd	|- ( ph -> ( ( X e. T /\ X e. ( ._|_ ` T ) ) -> X e. { .0. } ) )
17	10 16	mpand	|- ( ph -> ( X e. ( ._|_ ` T ) -> X e. { .0. } ) )
18	9 17	mtod	|- ( ph -> -. X e. ( ._|_ ` T ) )