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	$⊢ B = {Base}_{K}$
	lhpset.u	$⊢ \underset{˙}{1} = 1. (K)$
	lhpset.c	$⊢ C = ⋖_{K}$
	lhpset.h	$⊢ H = LHyp (K)$
Assertion	islhp2	$⊢ (K \in A \land W \in B) \to (W \in H \leftrightarrow W C \underset{˙}{1})$

Step	Hyp	Ref	Expression
1		lhpset.b	$⊢ B = {Base}_{K}$
2		lhpset.u	$⊢ \underset{˙}{1} = 1. (K)$
3		lhpset.c	$⊢ C = ⋖_{K}$
4		lhpset.h	$⊢ H = LHyp (K)$
5	1 2 3 4	islhp	$⊢ K \in A \to (W \in H \leftrightarrow (W \in B \land W C \underset{˙}{1}))$
6	5	baibd	$⊢ (K \in A \land W \in B) \to (W \in H \leftrightarrow W C \underset{˙}{1})$