Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlomcmcv Structured version   Unicode version

Theorem hlomcmcv 34030
Description: A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
hlomcmcv  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )

Proof of Theorem hlomcmcv
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2462 . . 3  |-  ( Base `  K )  =  (
Base `  K )
2 eqid 2462 . . 3  |-  ( le
`  K )  =  ( le `  K
)
3 eqid 2462 . . 3  |-  ( lt
`  K )  =  ( lt `  K
)
4 eqid 2462 . . 3  |-  ( join `  K )  =  (
join `  K )
5 eqid 2462 . . 3  |-  ( 0.
`  K )  =  ( 0. `  K
)
6 eqid 2462 . . 3  |-  ( 1.
`  K )  =  ( 1. `  K
)
7 eqid 2462 . . 3  |-  ( Atoms `  K )  =  (
Atoms `  K )
81, 2, 3, 4, 5, 6, 7ishlat1 34026 . 2  |-  ( 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 ) ) ) ) ) )
98simplbi 460 1  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968    e. wcel 1762    =/= wne 2657   A.wral 2809   E.wrex 2810   class class class wbr 4442   ` cfv 5581  (class class class)co 6277   Basecbs 14481   lecple 14553   ltcplt 15419   joincjn 15422   0.cp0 15515   1.cp1 15516   CLatccla 15585   OMLcoml 33849   Atomscatm 33937   CvLatclc 33939   HLchlt 34024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-hlat 34025
This theorem is referenced by:  hloml  34031  hlclat  34032  hlcvl  34033  cvr1  34083  cvrp  34089  atcvr1  34090  atcvr2  34091
  Copyright terms: Public domain W3C validator