This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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