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

Metamath Proof Explorer

Theorem lhpoc2N

Description: The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhpoc.b 
|- B = ( Base ` K )
lhpoc.o 
|- ._|_ = ( oc ` K )
lhpoc.a 
|- A = ( Atoms ` K )
lhpoc.h 
|- H = ( LHyp ` K )
Assertion lhpoc2N 
|- ( ( K e. HL /\ W e. B ) -> ( W e. A <-> ( ._|_ ` W ) e. H ) )

Proof

Step Hyp Ref Expression
1 lhpoc.b 
 |-  B = ( Base ` K )
2 lhpoc.o 
 |-  ._|_ = ( oc ` K )
3 lhpoc.a 
 |-  A = ( Atoms ` K )
4 lhpoc.h 
 |-  H = ( LHyp ` K )
5 hlop 
 |-  ( K e. HL -> K e. OP )
6 1 2 opoccl 
 |-  ( ( K e. OP /\ W e. B ) -> ( ._|_ ` W ) e. B )
7 5 6 sylan 
 |-  ( ( K e. HL /\ W e. B ) -> ( ._|_ ` W ) e. B )
8 1 2 3 4 lhpoc 
 |-  ( ( K e. HL /\ ( ._|_ ` W ) e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) )
9 7 8 syldan 
 |-  ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) )
10 1 2 opococ 
 |-  ( ( K e. OP /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W )
11 5 10 sylan 
 |-  ( ( K e. HL /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W )
12 11 eleq1d 
 |-  ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` ( ._|_ ` W ) ) e. A <-> W e. A ) )
13 9 12 bitr2d 
 |-  ( ( K e. HL /\ W e. B ) -> ( W e. A <-> ( ._|_ ` W ) e. H ) )