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

Theorem hlol 33006
Description: A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlol  |-  ( K  e.  HL  ->  K  e.  OL )

Proof of Theorem hlol
StepHypRef Expression
1 hloml 33002 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 32885 . 2  |-  ( K  e.  OML  ->  K  e.  OL )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  OL )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   OLcol 32819   OMLcoml 32820   HLchlt 32995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094  df-oml 32824  df-hlat 32996
This theorem is referenced by:  hlop  33007  cvrexch  33064  atle  33080  athgt  33100  2at0mat0  33169  dalem24  33341  pmapjat1  33497  atmod1i1m  33502  llnexchb2lem  33512  dalawlem2  33516  dalawlem6  33520  dalawlem7  33521  dalawlem11  33525  dalawlem12  33526  poldmj1N  33572  pmapj2N  33573  2polatN  33576  lhpmcvr3  33669  lhp2at0  33676  lhp2at0nle  33679  lhpelim  33681  lhpmod2i2  33682  lhpmod6i1  33683  lhprelat3N  33684  lhple  33686  4atex2-0aOLDN  33722  trljat1  33810  trljat2  33811  cdlemc1  33835  cdlemc6  33840  cdleme0cp  33858  cdleme0cq  33859  cdleme0e  33861  cdleme1  33871  cdleme2  33872  cdleme3c  33874  cdleme4  33882  cdleme5  33884  cdleme7c  33889  cdleme7e  33891  cdleme8  33894  cdleme9  33897  cdleme10  33898  cdleme15b  33919  cdlemednpq  33943  cdleme20y  33946  cdleme20c  33955  cdleme20d  33956  cdleme20j  33962  cdleme22cN  33986  cdleme22d  33987  cdleme22e  33988  cdleme22eALTN  33989  cdleme23b  33994  cdleme30a  34022  cdlemefrs29pre00  34039  cdlemefrs29bpre0  34040  cdlemefrs29cpre1  34042  cdleme32fva  34081  cdleme35b  34094  cdleme35d  34096  cdleme35e  34097  cdleme42a  34115  cdleme42ke  34129  cdlemeg46frv  34169  cdlemg2fv2  34244  cdlemg2m  34248  cdlemg10bALTN  34280  cdlemg12e  34291  cdlemg31d  34344  trlcoabs2N  34366  trlcolem  34370  trljco  34384  cdlemh2  34460  cdlemh  34461  cdlemi1  34462  cdlemk4  34478  cdlemk9  34483  cdlemk9bN  34484  cdlemkid2  34568  dia2dimlem1  34709  dia2dimlem2  34710  dia2dimlem3  34711  doca2N  34771  djajN  34782  cdlemn10  34851  dihvalcqat  34884  dih1  34931  dihglbcpreN  34945  dihmeetbclemN  34949  dihmeetlem7N  34955  dihjatc1  34956  djhlj  35046  djh01  35057  dihjatc  35062
  Copyright terms: Public domain W3C validator