hlomcmcv

Description: A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012)

		Ref	Expression
	Assertion	hlomcmcv	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in CvLat)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{K} = {Base}_{K}$
2		eqid	$⊢ \leq_{K} = \leq_{K}$
3		eqid	$⊢ <_{K} = <_{K}$
4		eqid	$⊢ join (K) = join (K)$
5		eqid	$⊢ 0. (K) = 0. (K)$
6		eqid	$⊢ 1. (K) = 1. (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	1 2 3 4 5 6 7	ishlat1	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in CvLat) \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 \exists x \in {Base}_{K} \exists y \in {Base}_{K} \exists z \in {Base}_{K} ((0. (K) <_{K} x \land x <_{K} y) \land (y <_{K} z \land z <_{K} 1. (K)))))$
9	8	simplbi	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in CvLat)$

Metamath Proof Explorer