Theorem islhp2

Description: The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	lhpset.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lhpset.u	⊢ 1 = ( 1. ‘ 𝐾 )
	lhpset.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	lhpset.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	islhp2	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐻 ↔ 𝑊 𝐶 1 ) )

Proof

Step	Hyp	Ref	Expression
1		lhpset.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lhpset.u	⊢ 1 = ( 1. ‘ 𝐾 )
3		lhpset.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		lhpset.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5	1 2 3 4	islhp	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ 𝐵 ∧ 𝑊 𝐶 1 ) ) )
6	5	baibd	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑊 ∈ 𝐻 ↔ 𝑊 𝐶 1 ) )