Metamath Proof Explorer


Theorem lhpoc

Description: The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses lhpoc.b B = Base K
lhpoc.o ˙ = oc K
lhpoc.a A = Atoms K
lhpoc.h H = LHyp K
Assertion lhpoc K HL W B W H ˙ W A

Proof

Step Hyp Ref Expression
1 lhpoc.b B = Base K
2 lhpoc.o ˙ = oc K
3 lhpoc.a A = Atoms K
4 lhpoc.h H = LHyp K
5 eqid 1. K = 1. K
6 eqid K = K
7 1 5 6 4 islhp2 K HL W B W H W K 1. K
8 1 5 2 6 3 1cvrco K HL W B W K 1. K ˙ W A
9 7 8 bitrd K HL W B W H ˙ W A