This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. } )