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 ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
3 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
4 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
5 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 1 2 3 4 5 6 7 ishlat1 ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝐾 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝐾 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ∃ 𝑦 ∈ ( Base ‘ 𝐾 ) ∃ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) ) )
9 8 simplbi ⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) )