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

Theorem hlol 34155
Description: A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlol (𝐾 ∈ HL → 𝐾 ∈ OL)

Proof of Theorem hlol
StepHypRef Expression
1 hloml 34151 . 2 (𝐾 ∈ HL → 𝐾 ∈ OML)
2 omlol 34034 . 2 (𝐾 ∈ OML → 𝐾 ∈ OL)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OL)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  OLcol 33968  OMLcoml 33969  HLchlt 34144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-oml 33973  df-hlat 34145
This theorem is referenced by:  hlop  34156  cvrexch  34213  atle  34229  athgt  34249  2at0mat0  34318  dalem24  34490  pmapjat1  34646  atmod1i1m  34651  llnexchb2lem  34661  dalawlem2  34665  dalawlem6  34669  dalawlem7  34670  dalawlem11  34674  dalawlem12  34675  poldmj1N  34721  pmapj2N  34722  2polatN  34725  lhpmcvr3  34818  lhp2at0  34825  lhp2at0nle  34828  lhpelim  34830  lhpmod2i2  34831  lhpmod6i1  34832  lhprelat3N  34833  lhple  34835  4atex2-0aOLDN  34871  trljat1  34960  trljat2  34961  cdlemc1  34985  cdlemc6  34990  cdleme0cp  35008  cdleme0cq  35009  cdleme0e  35011  cdleme1  35021  cdleme2  35022  cdleme3c  35024  cdleme4  35032  cdleme5  35034  cdleme7c  35039  cdleme7e  35041  cdleme8  35044  cdleme9  35047  cdleme10  35048  cdleme15b  35069  cdlemednpq  35093  cdleme20yOLD  35097  cdleme20c  35106  cdleme20d  35107  cdleme20j  35113  cdleme22cN  35137  cdleme22d  35138  cdleme22e  35139  cdleme22eALTN  35140  cdleme23b  35145  cdleme30a  35173  cdlemefrs29pre00  35190  cdlemefrs29bpre0  35191  cdlemefrs29cpre1  35193  cdleme32fva  35232  cdleme35b  35245  cdleme35d  35247  cdleme35e  35248  cdleme42a  35266  cdleme42ke  35280  cdlemeg46frv  35320  cdlemg2fv2  35395  cdlemg2m  35399  cdlemg10bALTN  35431  cdlemg12e  35442  cdlemg31d  35495  trlcoabs2N  35517  trlcolem  35521  trljco  35535  cdlemh2  35611  cdlemh  35612  cdlemi1  35613  cdlemk4  35629  cdlemk9  35634  cdlemk9bN  35635  cdlemkid2  35719  dia2dimlem1  35860  dia2dimlem2  35861  dia2dimlem3  35862  doca2N  35922  djajN  35933  cdlemn10  36002  dihvalcqat  36035  dih1  36082  dihglbcpreN  36096  dihmeetbclemN  36100  dihmeetlem7N  36106  dihjatc1  36107  djhlj  36197  djh01  36208  dihjatc  36213
  Copyright terms: Public domain W3C validator