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

Theorem hlol 30173
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 30169 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 30052 . 2  |-  ( K  e.  OML  ->  K  e.  OL )
31, 2syl 15 1  |-  ( K  e.  HL  ->  K  e.  OL )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   OLcol 29986   OMLcoml 29987   HLchlt 30162
This theorem is referenced by:  hlop  30174  cvrexch  30231  atle  30247  athgt  30267  2at0mat0  30336  dalem24  30508  pmapjat1  30664  atmod1i1m  30669  llnexchb2lem  30679  dalawlem2  30683  dalawlem6  30687  dalawlem7  30688  dalawlem11  30692  dalawlem12  30693  poldmj1N  30739  pmapj2N  30740  2polatN  30743  lhpmcvr3  30836  lhp2at0  30843  lhp2at0nle  30846  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  lhprelat3N  30851  lhple  30853  4atex2-0aOLDN  30889  trljat1  30977  trljat2  30978  cdlemc1  31002  cdlemc6  31007  cdleme0cp  31025  cdleme0cq  31026  cdleme0e  31028  cdleme1  31038  cdleme2  31039  cdleme3c  31041  cdleme4  31049  cdleme5  31051  cdleme7c  31056  cdleme7e  31058  cdleme8  31061  cdleme9  31064  cdleme10  31065  cdleme15b  31086  cdlemednpq  31110  cdleme20y  31113  cdleme20c  31122  cdleme20d  31123  cdleme20j  31129  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme23b  31161  cdleme30a  31189  cdlemefrs29pre00  31206  cdlemefrs29bpre0  31207  cdlemefrs29cpre1  31209  cdleme32fva  31248  cdleme35b  31261  cdleme35d  31263  cdleme35e  31264  cdleme42a  31282  cdleme42ke  31296  cdlemeg46frv  31336  cdlemg2fv2  31411  cdlemg2m  31415  cdlemg10bALTN  31447  cdlemg12e  31458  cdlemg31d  31511  trlcoabs2N  31533  trlcolem  31537  trljco  31551  cdlemh2  31627  cdlemh  31628  cdlemi1  31629  cdlemk4  31645  cdlemk9  31650  cdlemk9bN  31651  cdlemkid2  31735  dia2dimlem1  31876  dia2dimlem2  31877  dia2dimlem3  31878  doca2N  31938  djajN  31949  cdlemn10  32018  dihvalcqat  32051  dih1  32098  dihglbcpreN  32112  dihmeetbclemN  32116  dihmeetlem7N  32122  dihjatc1  32123  djhlj  32213  djh01  32224  dihjatc  32229
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-oml 29991  df-hlat 30163
  Copyright terms: Public domain W3C validator