Metamath Proof Explorer

Theorem dochshpsat

Description: A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochshpsat.h 
|- H = ( LHyp ` K )
dochshpsat.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochshpsat.u 
|- U = ( ( DVecH ` K ) ` W )
dochshpsat.a 
|- A = ( LSAtoms ` U )
dochshpsat.y 
|- Y = ( LSHyp ` U )
dochshpsat.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochshpsat.x 
|- ( ph -> X e. Y )
Assertion dochshpsat 
|- ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) = X <-> ( ._|_ ` X ) e. A ) )

Proof

Step Hyp Ref Expression
1 dochshpsat.h 
 |-  H = ( LHyp ` K )
2 dochshpsat.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochshpsat.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochshpsat.a 
 |-  A = ( LSAtoms ` U )
5 dochshpsat.y 
 |-  Y = ( LSHyp ` U )
6 dochshpsat.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 dochshpsat.x 
 |-  ( ph -> X e. Y )
8 simpr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
9 7 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> X e. Y )
10 8 9 eqeltrd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` ( ._|_ ` X ) ) e. Y )
11 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
12 1 3 6 dvhlmod 
 |-  ( ph -> U e. LMod )
13 11 5 12 7 lshplss 
 |-  ( ph -> X e. ( LSubSp ` U ) )
14 eqid 
 |-  ( Base ` U ) = ( Base ` U )
15 14 11 lssss 
 |-  ( X e. ( LSubSp ` U ) -> X C_ ( Base ` U ) )
16 13 15 syl 
 |-  ( ph -> X C_ ( Base ` U ) )
17 1 3 14 11 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` U ) ) -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
18 6 16 17 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
19 1 2 3 11 4 5 6 18 dochsatshpb 
 |-  ( ph -> ( ( ._|_ ` X ) e. A <-> ( ._|_ ` ( ._|_ ` X ) ) e. Y ) )
20 19 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ( ._|_ ` X ) e. A <-> ( ._|_ ` ( ._|_ ` X ) ) e. Y ) )
21 10 20 mpbird 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( ._|_ ` X ) e. A )
22 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
23 12 adantr 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> U e. LMod )
24 simpr 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ._|_ ` X ) e. A )
25 22 4 23 24 lsatn0 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ._|_ ` X ) =/= { ( 0g ` U ) } )
26 25 neneqd 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> -. ( ._|_ ` X ) = { ( 0g ` U ) } )
27 6 adantr 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( K e. HL /\ W e. H ) )
28 1 3 2 14 22 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = ( Base ` U ) )
29 27 28 syl 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ._|_ ` { ( 0g ` U ) } ) = ( Base ` U ) )
30 29 eqeq2d 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` { ( 0g ` U ) } ) <-> ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) ) )
31 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
32 1 31 3 14 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` U ) ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
33 6 16 32 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
34 1 31 3 22 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { ( 0g ` U ) } e. ran ( ( DIsoH ` K ) ` W ) )
35 6 34 syl 
 |-  ( ph -> { ( 0g ` U ) } e. ran ( ( DIsoH ` K ) ` W ) )
36 1 31 2 6 33 35 doch11 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` { ( 0g ` U ) } ) <-> ( ._|_ ` X ) = { ( 0g ` U ) } ) )
37 36 adantr 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` { ( 0g ` U ) } ) <-> ( ._|_ ` X ) = { ( 0g ` U ) } ) )
38 30 37 bitr3d 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) <-> ( ._|_ ` X ) = { ( 0g ` U ) } ) )
39 26 38 mtbird 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> -. ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) )
40 1 2 3 14 5 6 7 dochshpncl 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) =/= X <-> ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) ) )
41 40 necon1bbid 
 |-  ( ph -> ( -. ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) <-> ( ._|_ ` ( ._|_ ` X ) ) = X ) )
42 41 adantr 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( -. ( ._|_ ` ( ._|_ ` X ) ) = ( Base ` U ) <-> ( ._|_ ` ( ._|_ ` X ) ) = X ) )
43 39 42 mpbid 
 |-  ( ( ph /\ ( ._|_ ` X ) e. A ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
44 21 43 impbida 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) = X <-> ( ._|_ ` X ) e. A ) )