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 = Base K
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 = Base K
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