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 36602
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 36598 . 2 (𝐾 ∈ HL → 𝐾 ∈ OML)
2 omlol 36481 . 2 (𝐾 ∈ OML → 𝐾 ∈ OL)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OL)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  OLcol 36415  OMLcoml 36416  HLchlt 36591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152  df-oml 36420  df-hlat 36592
This theorem is referenced by:  hlop  36603  cvrexch  36661  atle  36677  athgt  36697  2at0mat0  36766  dalem24  36938  pmapjat1  37094  atmod1i1m  37099  llnexchb2lem  37109  dalawlem2  37113  dalawlem6  37117  dalawlem7  37118  dalawlem11  37122  dalawlem12  37123  poldmj1N  37169  pmapj2N  37170  2polatN  37173  lhpmcvr3  37266  lhp2at0  37273  lhp2at0nle  37276  lhpelim  37278  lhpmod2i2  37279  lhpmod6i1  37280  lhprelat3N  37281  lhple  37283  4atex2-0aOLDN  37319  trljat1  37407  trljat2  37408  cdlemc1  37432  cdlemc6  37437  cdleme0cp  37455  cdleme0cq  37456  cdleme0e  37458  cdleme1  37468  cdleme2  37469  cdleme3c  37471  cdleme4  37479  cdleme5  37481  cdleme7c  37486  cdleme7e  37488  cdleme8  37491  cdleme9  37494  cdleme10  37495  cdleme15b  37516  cdlemednpq  37540  cdleme20c  37552  cdleme20d  37553  cdleme20j  37559  cdleme22cN  37583  cdleme22d  37584  cdleme22e  37585  cdleme22eALTN  37586  cdleme23b  37591  cdleme30a  37619  cdlemefrs29pre00  37636  cdlemefrs29bpre0  37637  cdlemefrs29cpre1  37639  cdleme32fva  37678  cdleme35b  37691  cdleme35d  37693  cdleme35e  37694  cdleme42a  37712  cdleme42ke  37726  cdlemeg46frv  37766  cdlemg2fv2  37841  cdlemg2m  37845  cdlemg10bALTN  37877  cdlemg12e  37888  cdlemg31d  37941  trlcoabs2N  37963  trlcolem  37967  trljco  37981  cdlemh2  38057  cdlemh  38058  cdlemi1  38059  cdlemk4  38075  cdlemk9  38080  cdlemk9bN  38081  cdlemkid2  38165  dia2dimlem1  38305  dia2dimlem2  38306  dia2dimlem3  38307  doca2N  38367  djajN  38378  cdlemn10  38447  dihvalcqat  38480  dih1  38527  dihglbcpreN  38541  dihmeetbclemN  38545  dihmeetlem7N  38551  dihjatc1  38552  djhlj  38642  djh01  38653  dihjatc  38658
  Copyright terms: Public domain W3C validator