Theorem islhp2

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

	Ref	Expression
Hypotheses	lhpset.b	$$⊢B={\mathrm{Base}}_K$$
	lhpset.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	lhpset.c	$$⊢C={⋖}_K$$
	lhpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	islhp2	$$⊢\left(K\in A\wedge W\in B\right)\to \left(W\in H\leftrightarrow WC\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lhpset.b	$$⊢B={\mathrm{Base}}_K$$
2		lhpset.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
3		lhpset.c	$$⊢C={⋖}_K$$
4		lhpset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5	1 2 3 4	islhp	$$⊢K\in A\to \left(W\in H\leftrightarrow \left(W\in B\wedge WC\underset{\dot{}}{1}\right)\right)$$
6	5	baibd	$$⊢\left(K\in A\wedge W\in B\right)\to \left(W\in H\leftrightarrow WC\underset{\dot{}}{1}\right)$$