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 e. HL -> ( K e. OML /\ K e. CLat /\ K e. CvLat ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( le ` K ) = ( le ` K )
3 eqid 
 |-  ( lt ` K ) = ( lt ` 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 e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. ( Atoms ` K ) A. y e. ( Atoms ` K ) ( x =/= y -> E. z e. ( Atoms ` K ) ( z =/= x /\ z =/= y /\ z ( le ` K ) ( x ( join ` K ) y ) ) ) /\ E. x e. ( Base ` K ) E. y e. ( Base ` K ) E. z e. ( Base ` K ) ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) ) )
9 8 simplbi 
 |-  ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. CvLat ) )