Theorem lhpoc2N

Description: The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

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

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		hlop	|- ( K e. HL -> K e. OP )
6	1 2	opoccl	|- ( ( K e. OP /\ W e. B ) -> ( ._|_ ` W ) e. B )
7	5 6	sylan	|- ( ( K e. HL /\ W e. B ) -> ( ._|_ ` W ) e. B )
8	1 2 3 4	lhpoc	|- ( ( K e. HL /\ ( ._|_ ` W ) e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) )
9	7 8	syldan	|- ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` W ) e. H <-> ( ._|_ ` ( ._|_ ` W ) ) e. A ) )
10	1 2	opococ	|- ( ( K e. OP /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W )
11	5 10	sylan	|- ( ( K e. HL /\ W e. B ) -> ( ._|_ ` ( ._|_ ` W ) ) = W )
12	11	eleq1d	|- ( ( K e. HL /\ W e. B ) -> ( ( ._|_ ` ( ._|_ ` W ) ) e. A <-> W e. A ) )
13	9 12	bitr2d	|- ( ( K e. HL /\ W e. B ) -> ( W e. A <-> ( ._|_ ` W ) e. H ) )