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 ) ) |
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 ) ) |