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