Theorem islhp

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

	Ref	Expression
Hypotheses	lhpset.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lhpset.u	⊢ 1 = ( 1. ‘ 𝐾 )
	lhpset.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	lhpset.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	islhp	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ 𝐵 ∧ 𝑊 𝐶 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	lhpset	⊢ ( 𝐾 ∈ 𝐴 → 𝐻 = { 𝑤 ∈ 𝐵 ∣ 𝑤 𝐶 1 } )
6	5	eleq2d	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑊 ∈ 𝐻 ↔ 𝑊 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝐶 1 } ) )
7		breq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 𝐶 1 ↔ 𝑊 𝐶 1 ) )
8	7	elrab	⊢ ( 𝑊 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑤 𝐶 1 } ↔ ( 𝑊 ∈ 𝐵 ∧ 𝑊 𝐶 1 ) )
9	6 8	bitrdi	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ 𝐵 ∧ 𝑊 𝐶 1 ) ) )