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

Metamath Proof Explorer

Theorem hlhgt4

Description: A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011)

		Ref	Expression
	Hypotheses	hlhgt4.b	$⊢ B = {Base}_{K}$
		hlhgt4.s	$⊢ \underset{˙}{<} = <_{K}$
		hlhgt4.z	$⊢ \underset{˙}{0} = 0. (K)$
		hlhgt4.u	$⊢ \underset{˙}{1} = 1. (K)$
	Assertion	hlhgt4	$⊢ K \in HL \to \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		hlhgt4.b	$⊢ B = {Base}_{K}$
2		hlhgt4.s	$⊢ \underset{˙}{<} = <_{K}$
3		hlhgt4.z	$⊢ \underset{˙}{0} = 0. (K)$
4		hlhgt4.u	$⊢ \underset{˙}{1} = 1. (K)$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6		eqid	$⊢ join (K) = join (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	1 5 2 6 3 4 7	ishlat2	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in AtLat) \land (\forall x \in Atoms (K) \forall y \in Atoms (K) ((x \neq y \to \exists z \in Atoms (K) (z \neq x \land z \neq y \land z \leq_{K} (x join (K) y))) \land \forall z \in B ((\neg x \leq_{K} z \land x \leq_{K} (z join (K) y)) \to y \leq_{K} (z join (K) x))) \land \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))))$
9		simprr	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land (\forall x \in Atoms (K) \forall y \in Atoms (K) ((x \neq y \to \exists z \in Atoms (K) (z \neq x \land z \neq y \land z \leq_{K} (x join (K) y))) \land \forall z \in B ((\neg x \leq_{K} z \land x \leq_{K} (z join (K) y)) \to y \leq_{K} (z join (K) x))) \land \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})))) \to \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$
10	8 9	sylbi	$⊢ K \in HL \to \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$