Theorem lhp1cvr

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

	Ref	Expression
Hypotheses	lhp1cvr.u	|- .1. = ( 1. ` K )
	lhp1cvr.c	|- C = (
	lhp1cvr.h	|- H = ( LHyp ` K )
Assertion	lhp1cvr	|- ( ( K e. A /\ W e. H ) -> W C .1. )

Proof

Step	Hyp	Ref	Expression
1		lhp1cvr.u	|- .1. = ( 1. ` K )
2		lhp1cvr.c	|- C = (
3		lhp1cvr.h	|- H = ( LHyp ` K )
4		eqid	|- ( Base ` K ) = ( Base ` K )
5	4 1 2 3	islhp	|- ( K e. A -> ( W e. H <-> ( W e. ( Base ` K ) /\ W C .1. ) ) )
6	5	simplbda	|- ( ( K e. A /\ W e. H ) -> W C .1. )