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

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpoc.o ⊢ ⊥ = ( oc ‘ 𝐾 )
lhpoc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpoc2N ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐴 ↔ ( ⊥ ‘ 𝑊 ) ∈ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 lhpoc.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpoc.o ⊢ ⊥ = ( oc ‘ 𝐾 )
3 lhpoc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lhpoc.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
6 1 2 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵 ) → ( ⊥ ‘ 𝑊 ) ∈ 𝐵 )
7 5 6 sylan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( ⊥ ‘ 𝑊 ) ∈ 𝐵 )
8 1 2 3 4 lhpoc ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ 𝑊 ) ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑊 ) ∈ 𝐻 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑊 ) ) ∈ 𝐴 ) )
9 7 8 syldan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑊 ) ∈ 𝐻 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑊 ) ) ∈ 𝐴 ) )
10 1 2 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑊 ) ) = 𝑊 )
11 5 10 sylan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑊 ) ) = 𝑊 )
12 11 eleq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑊 ) ) ∈ 𝐴 ↔ 𝑊 ∈ 𝐴 ) )
13 9 12 bitr2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐴 ↔ ( ⊥ ‘ 𝑊 ) ∈ 𝐻 ) )