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

Metamath Proof Explorer

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 )