Theorem lhpoc

Description: The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012)

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

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		eqid	|- ( 1. ` K ) = ( 1. ` K )
6		eqid	|- (
7	1 5 6 4	islhp2	|- ( ( K e. HL /\ W e. B ) -> ( W e. H <-> W (
8	1 5 2 6 3	1cvrco	|- ( ( K e. HL /\ W e. B ) -> ( W ( ( ._|_ ` W ) e. A ) )
9	7 8	bitrd	|- ( ( K e. HL /\ W e. B ) -> ( W e. H <-> ( ._|_ ` W ) e. A ) )