Theorem 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 \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
2		eqid	$$⊢{\le }_K={\le }_K$$
3		eqid	$$⊢{<}_K={<}_K$$
4		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
5		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
6		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
7		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
8	1 2 3 4 5 6 7	ishlat1	$$⊢K\in \mathrm{HL}\leftrightarrow \left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)\wedge \left(\forall x\in \mathrm{Atoms}\left(K\right)\forall y\in \mathrm{Atoms}\left(K\right)\left(x\ne y\to \exists z\in \mathrm{Atoms}\left(K\right)\left(z\ne x\wedge z\ne y\wedge z{\le }_K\left(x\mathrm{join}\left(K\right)y\right)\right)\right)\wedge \exists x\in {\mathrm{Base}}_K\exists y\in {\mathrm{Base}}_K\exists z\in {\mathrm{Base}}_K\left(\left(\mathrm{0.}\left(K\right){<}_{K}x\wedge x{<}_{K}y\right)\wedge \left(y{<}_{K}z\wedge z{<}_K\mathrm{1.}\left(K\right)\right)\right)\right)\right)$$
9	8	simplbi	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{CvLat}\right)$$