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

Proof

Step	Hyp	Ref	Expression
1		lhpoc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lhpoc.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3		lhpoc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		lhpoc.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
6		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
7	1 5 6 4	islhp2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐻 ↔ 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
8	1 5 2 6 3	1cvrco	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ↔ ( ⊥ ‘ 𝑊 ) ∈ 𝐴 ) )
9	7 8	bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐻 ↔ ( ⊥ ‘ 𝑊 ) ∈ 𝐴 ) )