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

Metamath Proof Explorer

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 ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base K = Base K
2 eqid ⊢ ≤ K = ≤ 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 ∈ HL ↔ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ ∀ x ∈ Atoms ⁡ K ∀ y ∈ Atoms ⁡ K x ≠ y → ∃ z ∈ Atoms ⁡ K z ≠ x ∧ z ≠ y ∧ z ≤ K x join ⁡ K y ∧ ∃ x ∈ Base K ∃ y ∈ Base K ∃ z ∈ Base K 0. ⁡ K < K x ∧ x < K y ∧ y < K z ∧ z < K 1. ⁡ K
9 8 simplbi ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat