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

Metamath Proof Explorer

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 ) )