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={\mathrm{Base}}_K$$
	lhpoc.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	lhpoc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhpoc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpoc	$$⊢\left(K\in \mathrm{HL}\wedge W\in B\right)\to \left(W\in H\leftrightarrow \underset{\dot{}}{\perp }\left(W\right)\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		lhpoc.b	$$⊢B={\mathrm{Base}}_K$$
2		lhpoc.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
3		lhpoc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lhpoc.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
6		eqid	$$⊢{⋖}_K={⋖}_K$$
7	1 5 6 4	islhp2	$$⊢\left(K\in \mathrm{HL}\wedge W\in B\right)\to \left(W\in H\leftrightarrow W{⋖}_K\mathrm{1.}\left(K\right)\right)$$
8	1 5 2 6 3	1cvrco	$$⊢\left(K\in \mathrm{HL}\wedge W\in B\right)\to \left(W{⋖}_K\mathrm{1.}\left(K\right)\leftrightarrow \underset{\dot{}}{\perp }\left(W\right)\in A\right)$$
9	7 8	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge W\in B\right)\to \left(W\in H\leftrightarrow \underset{\dot{}}{\perp }\left(W\right)\in A\right)$$