Theorem lhpocnel

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		lhpocnel.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lhpocnel.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
3		lhpocnel.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lhpocnel.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5	2 3 4	lhpocat	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(W\right)\in A$$
6	1 2 4	lhpocnle	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \neg \underset{\dot{}}{\perp }\left(W\right)\underset{\dot{}}{\le }W$$
7	5 6	jca	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \left(\underset{\dot{}}{\perp }\left(W\right)\in A\wedge \neg \underset{\dot{}}{\perp }\left(W\right)\underset{\dot{}}{\le }W\right)$$