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 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐴 ↔ ( ⊥ ‘ 𝑊 ) ∈ 𝐻 ) )