Metamath Proof Explorer


Theorem islhp

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

Ref Expression
Hypotheses lhpset.b
|- B = ( Base ` K )
lhpset.u
|- .1. = ( 1. ` K )
lhpset.c
|- C = ( 
lhpset.h
|- H = ( LHyp ` K )
Assertion islhp
|- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )

Proof

Step Hyp Ref Expression
1 lhpset.b
 |-  B = ( Base ` K )
2 lhpset.u
 |-  .1. = ( 1. ` K )
3 lhpset.c
 |-  C = ( 
4 lhpset.h
 |-  H = ( LHyp ` K )
5 1 2 3 4 lhpset
 |-  ( K e. A -> H = { w e. B | w C .1. } )
6 5 eleq2d
 |-  ( K e. A -> ( W e. H <-> W e. { w e. B | w C .1. } ) )
7 breq1
 |-  ( w = W -> ( w C .1. <-> W C .1. ) )
8 7 elrab
 |-  ( W e. { w e. B | w C .1. } <-> ( W e. B /\ W C .1. ) )
9 6 8 bitrdi
 |-  ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )