Metamath Proof Explorer

Theorem lhpoc2N

Description: The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhpoc.b ⊢B=BaseK
lhpoc.o ⊢⊥˙=oc⁡K
lhpoc.a ⊢A=Atoms⁡K
lhpoc.h ⊢H=LHyp⁡K
Assertion lhpoc2N ⊢K∈HL∧W∈B→W∈A↔⊥˙⁡W∈H

Proof

Step Hyp Ref Expression
1 lhpoc.b ⊢B=BaseK
2 lhpoc.o ⊢⊥˙=oc⁡K
3 lhpoc.a ⊢A=Atoms⁡K
4 lhpoc.h ⊢H=LHyp⁡K
5 hlop ⊢K∈HL→K∈OP
6 1 2 opoccl ⊢K∈OP∧W∈B→⊥˙⁡W∈B
7 5 6 sylan ⊢K∈HL∧W∈B→⊥˙⁡W∈B
8 1 2 3 4 lhpoc ⊢K∈HL∧⊥˙⁡W∈B→⊥˙⁡W∈H↔⊥˙⁡⊥˙⁡W∈A
9 7 8 syldan ⊢K∈HL∧W∈B→⊥˙⁡W∈H↔⊥˙⁡⊥˙⁡W∈A
10 1 2 opococ ⊢K∈OP∧W∈B→⊥˙⁡⊥˙⁡W=W
11 5 10 sylan ⊢K∈HL∧W∈B→⊥˙⁡⊥˙⁡W=W
12 11 eleq1d ⊢K∈HL∧W∈B→⊥˙⁡⊥˙⁡W∈A↔W∈A
13 9 12 bitr2d ⊢K∈HL∧W∈B→W∈A↔⊥˙⁡W∈H