Theorem lhpocat

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

	Ref	Expression
Hypotheses	lhpocat.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	lhpocat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lhpocat.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	lhpocat	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(W\right)\in A$$

Proof

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