Theorem lhp1cvr

Description: The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012)

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

Proof

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