Metamath Proof Explorer


Theorem lhpocnel

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses lhpocnel.l
|- .<_ = ( le ` K )
lhpocnel.o
|- ._|_ = ( oc ` K )
lhpocnel.a
|- A = ( Atoms ` K )
lhpocnel.h
|- H = ( LHyp ` K )
Assertion lhpocnel
|- ( ( K e. HL /\ W e. H ) -> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) .<_ W ) )

Proof

Step Hyp Ref Expression
1 lhpocnel.l
 |-  .<_ = ( le ` K )
2 lhpocnel.o
 |-  ._|_ = ( oc ` K )
3 lhpocnel.a
 |-  A = ( Atoms ` K )
4 lhpocnel.h
 |-  H = ( LHyp ` K )
5 2 3 4 lhpocat
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` W ) e. A )
6 1 2 4 lhpocnle
 |-  ( ( K e. HL /\ W e. H ) -> -. ( ._|_ ` W ) .<_ W )
7 5 6 jca
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) .<_ W ) )