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

Theorem hlol 29551
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 29547 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 29430 . 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 1684   OLcol 29364   OMLcoml 29365   HLchlt 29540
This theorem is referenced by:  hlop  29552  cvrexch  29609  atle  29625  athgt  29645  2at0mat0  29714  dalem24  29886  pmapjat1  30042  atmod1i1m  30047  llnexchb2lem  30057  dalawlem2  30061  dalawlem6  30065  dalawlem7  30066  dalawlem11  30070  dalawlem12  30071  poldmj1N  30117  pmapj2N  30118  2polatN  30121  lhpmcvr3  30214  lhp2at0  30221  lhp2at0nle  30224  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  lhprelat3N  30229  lhple  30231  4atex2-0aOLDN  30267  trljat1  30355  trljat2  30356  cdlemc1  30380  cdlemc6  30385  cdleme0cp  30403  cdleme0cq  30404  cdleme0e  30406  cdleme1  30416  cdleme2  30417  cdleme3c  30419  cdleme4  30427  cdleme5  30429  cdleme7c  30434  cdleme7e  30436  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme15b  30464  cdlemednpq  30488  cdleme20y  30491  cdleme20c  30500  cdleme20d  30501  cdleme20j  30507  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme23b  30539  cdleme30a  30567  cdlemefrs29pre00  30584  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdleme32fva  30626  cdleme35b  30639  cdleme35d  30641  cdleme35e  30642  cdleme42a  30660  cdleme42ke  30674  cdlemeg46frv  30714  cdlemg2fv2  30789  cdlemg2m  30793  cdlemg10bALTN  30825  cdlemg12e  30836  cdlemg31d  30889  trlcoabs2N  30911  trlcolem  30915  trljco  30929  cdlemh2  31005  cdlemh  31006  cdlemi1  31007  cdlemk4  31023  cdlemk9  31028  cdlemk9bN  31029  cdlemkid2  31113  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  doca2N  31316  djajN  31327  cdlemn10  31396  dihvalcqat  31429  dih1  31476  dihglbcpreN  31490  dihmeetbclemN  31494  dihmeetlem7N  31500  dihjatc1  31501  djhlj  31591  djh01  31602  dihjatc  31607
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-oml 29369  df-hlat 29541
  Copyright terms: Public domain W3C validator