Theorem islhp

Description: The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-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	islhp	$$⊢K\in A\to \left(W\in H\leftrightarrow \left(W\in B\wedge WC\underset{\dot{}}{1}\right)\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	lhpset	$$⊢K\in A\to H=\left\{w\in B|wC\underset{\dot{}}{1}\right\}$$
6	5	eleq2d	$$⊢K\in A\to \left(W\in H\leftrightarrow W\in \left\{w\in B|wC\underset{\dot{}}{1}\right\}\right)$$
7		breq1	$$⊢w=W\to \left(wC\underset{\dot{}}{1}\leftrightarrow WC\underset{\dot{}}{1}\right)$$
8	7	elrab	$$⊢W\in \left\{w\in B|wC\underset{\dot{}}{1}\right\}\leftrightarrow \left(W\in B\wedge WC\underset{\dot{}}{1}\right)$$
9	6 8	bitrdi	$$⊢K\in A\to \left(W\in H\leftrightarrow \left(W\in B\wedge WC\underset{\dot{}}{1}\right)\right)$$