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=BaseK
lhpset.u 1˙=1.K
lhpset.c C=K
lhpset.h H=LHypK
Assertion islhp KAWHWBWC1˙

Proof

Step Hyp Ref Expression
1 lhpset.b B=BaseK
2 lhpset.u 1˙=1.K
3 lhpset.c C=K
4 lhpset.h H=LHypK
5 1 2 3 4 lhpset KAH=wB|wC1˙
6 5 eleq2d KAWHWwB|wC1˙
7 breq1 w=WwC1˙WC1˙
8 7 elrab WwB|wC1˙WBWC1˙
9 6 8 bitrdi KAWHWBWC1˙