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

Theorem hlol 32635
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 32631 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 32514 . 2  |-  ( K  e.  OML  ->  K  e.  OL )
31, 2syl 17 1  |-  ( K  e.  HL  ->  K  e.  OL )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   OLcol 32448   OMLcoml 32449   HLchlt 32624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-oml 32453  df-hlat 32625
This theorem is referenced by:  hlop  32636  cvrexch  32693  atle  32709  athgt  32729  2at0mat0  32798  dalem24  32970  pmapjat1  33126  atmod1i1m  33131  llnexchb2lem  33141  dalawlem2  33145  dalawlem6  33149  dalawlem7  33150  dalawlem11  33154  dalawlem12  33155  poldmj1N  33201  pmapj2N  33202  2polatN  33205  lhpmcvr3  33298  lhp2at0  33305  lhp2at0nle  33308  lhpelim  33310  lhpmod2i2  33311  lhpmod6i1  33312  lhprelat3N  33313  lhple  33315  4atex2-0aOLDN  33351  trljat1  33440  trljat2  33441  cdlemc1  33465  cdlemc6  33470  cdleme0cp  33488  cdleme0cq  33489  cdleme0e  33491  cdleme1  33501  cdleme2  33502  cdleme3c  33504  cdleme4  33512  cdleme5  33514  cdleme7c  33519  cdleme7e  33521  cdleme8  33524  cdleme9  33527  cdleme10  33528  cdleme15b  33549  cdlemednpq  33573  cdleme20yOLD  33577  cdleme20c  33586  cdleme20d  33587  cdleme20j  33593  cdleme22cN  33617  cdleme22d  33618  cdleme22e  33619  cdleme22eALTN  33620  cdleme23b  33625  cdleme30a  33653  cdlemefrs29pre00  33670  cdlemefrs29bpre0  33671  cdlemefrs29cpre1  33673  cdleme32fva  33712  cdleme35b  33725  cdleme35d  33727  cdleme35e  33728  cdleme42a  33746  cdleme42ke  33760  cdlemeg46frv  33800  cdlemg2fv2  33875  cdlemg2m  33879  cdlemg10bALTN  33911  cdlemg12e  33922  cdlemg31d  33975  trlcoabs2N  33997  trlcolem  34001  trljco  34015  cdlemh2  34091  cdlemh  34092  cdlemi1  34093  cdlemk4  34109  cdlemk9  34114  cdlemk9bN  34115  cdlemkid2  34199  dia2dimlem1  34340  dia2dimlem2  34341  dia2dimlem3  34342  doca2N  34402  djajN  34413  cdlemn10  34482  dihvalcqat  34515  dih1  34562  dihglbcpreN  34576  dihmeetbclemN  34580  dihmeetlem7N  34586  dihjatc1  34587  djhlj  34677  djh01  34688  dihjatc  34693
  Copyright terms: Public domain W3C validator