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

Metamath Proof Explorer

Theorem dochn0nv

Description: An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 dochn0nv.h 
 |-  H = ( LHyp ` K )
2 dochn0nv.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochn0nv.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochn0nv.v 
 |-  V = ( Base ` U )
5 dochn0nv.z 
 |-  .0. = ( 0g ` U )
6 dochn0nv.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 dochn0nv.x 
 |-  ( ph -> X C_ V )
8 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
9 1 8 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
10 6 7 9 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
11 1 8 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
12 6 10 11 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` X ) )
13 1 3 2 4 5 doch1 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` V ) = { .0. } )
14 6 13 syl 
 |-  ( ph -> ( ._|_ ` V ) = { .0. } )
15 12 14 eqeq12d 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` V ) <-> ( ._|_ ` X ) = { .0. } ) )
16 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) C_ V )
17 6 7 16 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) C_ V )
18 1 8 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
19 6 17 18 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
20 1 8 3 4 dih1rn 
 |-  ( ( K e. HL /\ W e. H ) -> V e. ran ( ( DIsoH ` K ) ` W ) )
21 6 20 syl 
 |-  ( ph -> V e. ran ( ( DIsoH ` K ) ` W ) )
22 1 8 2 6 19 21 doch11 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` V ) <-> ( ._|_ ` ( ._|_ ` X ) ) = V ) )
23 15 22 bitr3d 
 |-  ( ph -> ( ( ._|_ ` X ) = { .0. } <-> ( ._|_ ` ( ._|_ ` X ) ) = V ) )
24 23 necon3bid 
 |-  ( ph -> ( ( ._|_ ` X ) =/= { .0. } <-> ( ._|_ ` ( ._|_ ` X ) ) =/= V ) )