Theorem lhpocat

Description: The orthocomplement of a co-atom is an atom. (Contributed by NM, 9-Feb-2013)

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

Proof

Step	Hyp	Ref	Expression
1		lhpocat.o	|- ._|_ = ( oc ` K )
2		lhpocat.a	|- A = ( Atoms ` K )
3		lhpocat.h	|- H = ( LHyp ` K )
4		simpr	|- ( ( K e. HL /\ W e. H ) -> W e. H )
5		eqid	|- ( Base ` K ) = ( Base ` K )
6	5 3	lhpbase	|- ( W e. H -> W e. ( Base ` K ) )
7	5 1 2 3	lhpoc	|- ( ( K e. HL /\ W e. ( Base ` K ) ) -> ( W e. H <-> ( ._|_ ` W ) e. A ) )
8	6 7	sylan2	|- ( ( K e. HL /\ W e. H ) -> ( W e. H <-> ( ._|_ ` W ) e. A ) )
9	4 8	mpbid	|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` W ) e. A )