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 37869
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 37865 . 2 (𝐾 ∈ HL → 𝐾 ∈ OML)
2 omlol 37748 . 2 (𝐾 ∈ OML → 𝐾 ∈ OL)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OL)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  OLcol 37682  OMLcoml 37683  HLchlt 37858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-oml 37687  df-hlat 37859
This theorem is referenced by:  hlop  37870  cvrexch  37929  atle  37945  athgt  37965  2at0mat0  38034  dalem24  38206  pmapjat1  38362  atmod1i1m  38367  llnexchb2lem  38377  dalawlem2  38381  dalawlem6  38385  dalawlem7  38386  dalawlem11  38390  dalawlem12  38391  poldmj1N  38437  pmapj2N  38438  2polatN  38441  lhpmcvr3  38534  lhp2at0  38541  lhp2at0nle  38544  lhpelim  38546  lhpmod2i2  38547  lhpmod6i1  38548  lhprelat3N  38549  lhple  38551  4atex2-0aOLDN  38587  trljat1  38675  trljat2  38676  cdlemc1  38700  cdlemc6  38705  cdleme0cp  38723  cdleme0cq  38724  cdleme0e  38726  cdleme1  38736  cdleme2  38737  cdleme3c  38739  cdleme4  38747  cdleme5  38749  cdleme7c  38754  cdleme7e  38756  cdleme8  38759  cdleme9  38762  cdleme10  38763  cdleme15b  38784  cdlemednpq  38808  cdleme20c  38820  cdleme20d  38821  cdleme20j  38827  cdleme22cN  38851  cdleme22d  38852  cdleme22e  38853  cdleme22eALTN  38854  cdleme23b  38859  cdleme30a  38887  cdlemefrs29pre00  38904  cdlemefrs29bpre0  38905  cdlemefrs29cpre1  38907  cdleme32fva  38946  cdleme35b  38959  cdleme35d  38961  cdleme35e  38962  cdleme42a  38980  cdleme42ke  38994  cdlemeg46frv  39034  cdlemg2fv2  39109  cdlemg2m  39113  cdlemg10bALTN  39145  cdlemg12e  39156  cdlemg31d  39209  trlcoabs2N  39231  trlcolem  39235  trljco  39249  cdlemh2  39325  cdlemh  39326  cdlemi1  39327  cdlemk4  39343  cdlemk9  39348  cdlemk9bN  39349  cdlemkid2  39433  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575  doca2N  39635  djajN  39646  cdlemn10  39715  dihvalcqat  39748  dih1  39795  dihglbcpreN  39809  dihmeetbclemN  39813  dihmeetlem7N  39819  dihjatc1  39820  djhlj  39910  djh01  39921  dihjatc  39926
  Copyright terms: Public domain W3C validator