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

Theorem hlol 29478
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 29474 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 29357 . 2  |-  ( K  e.  OML  ->  K  e.  OL )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  OL )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   OLcol 29291   OMLcoml 29292   HLchlt 29467
This theorem is referenced by:  hlop  29479  cvrexch  29536  atle  29552  athgt  29572  2at0mat0  29641  dalem24  29813  pmapjat1  29969  atmod1i1m  29974  llnexchb2lem  29984  dalawlem2  29988  dalawlem6  29992  dalawlem7  29993  dalawlem11  29997  dalawlem12  29998  poldmj1N  30044  pmapj2N  30045  2polatN  30048  lhpmcvr3  30141  lhp2at0  30148  lhp2at0nle  30151  lhpelim  30153  lhpmod2i2  30154  lhpmod6i1  30155  lhprelat3N  30156  lhple  30158  4atex2-0aOLDN  30194  trljat1  30282  trljat2  30283  cdlemc1  30307  cdlemc6  30312  cdleme0cp  30330  cdleme0cq  30331  cdleme0e  30333  cdleme1  30343  cdleme2  30344  cdleme3c  30346  cdleme4  30354  cdleme5  30356  cdleme7c  30361  cdleme7e  30363  cdleme8  30366  cdleme9  30369  cdleme10  30370  cdleme15b  30391  cdlemednpq  30415  cdleme20y  30418  cdleme20c  30427  cdleme20d  30428  cdleme20j  30434  cdleme22cN  30458  cdleme22d  30459  cdleme22e  30460  cdleme22eALTN  30461  cdleme23b  30466  cdleme30a  30494  cdlemefrs29pre00  30511  cdlemefrs29bpre0  30512  cdlemefrs29cpre1  30514  cdleme32fva  30553  cdleme35b  30566  cdleme35d  30568  cdleme35e  30569  cdleme42a  30587  cdleme42ke  30601  cdlemeg46frv  30641  cdlemg2fv2  30716  cdlemg2m  30720  cdlemg10bALTN  30752  cdlemg12e  30763  cdlemg31d  30816  trlcoabs2N  30838  trlcolem  30842  trljco  30856  cdlemh2  30932  cdlemh  30933  cdlemi1  30934  cdlemk4  30950  cdlemk9  30955  cdlemk9bN  30956  cdlemkid2  31040  dia2dimlem1  31181  dia2dimlem2  31182  dia2dimlem3  31183  doca2N  31243  djajN  31254  cdlemn10  31323  dihvalcqat  31356  dih1  31403  dihglbcpreN  31417  dihmeetbclemN  31421  dihmeetlem7N  31427  dihjatc1  31428  djhlj  31518  djh01  31529  dihjatc  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-iota 5360  df-fv 5404  df-ov 6025  df-oml 29296  df-hlat 29468
  Copyright terms: Public domain W3C validator