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 ) )