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

Theorem hlol 34167
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 34163 . 2  |-  ( K  e.  HL  ->  K  e.  OML )
2 omlol 34046 . 2  |-  ( K  e.  OML  ->  K  e.  OL )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  OL )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   OLcol 33980   OMLcoml 33981   HLchlt 34156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5550  df-fv 5595  df-ov 6286  df-oml 33985  df-hlat 34157
This theorem is referenced by:  hlop  34168  cvrexch  34225  atle  34241  athgt  34261  2at0mat0  34330  dalem24  34502  pmapjat1  34658  atmod1i1m  34663  llnexchb2lem  34673  dalawlem2  34677  dalawlem6  34681  dalawlem7  34682  dalawlem11  34686  dalawlem12  34687  poldmj1N  34733  pmapj2N  34734  2polatN  34737  lhpmcvr3  34830  lhp2at0  34837  lhp2at0nle  34840  lhpelim  34842  lhpmod2i2  34843  lhpmod6i1  34844  lhprelat3N  34845  lhple  34847  4atex2-0aOLDN  34883  trljat1  34971  trljat2  34972  cdlemc1  34996  cdlemc6  35001  cdleme0cp  35019  cdleme0cq  35020  cdleme0e  35022  cdleme1  35032  cdleme2  35033  cdleme3c  35035  cdleme4  35043  cdleme5  35045  cdleme7c  35050  cdleme7e  35052  cdleme8  35055  cdleme9  35058  cdleme10  35059  cdleme15b  35080  cdlemednpq  35104  cdleme20y  35107  cdleme20c  35116  cdleme20d  35117  cdleme20j  35123  cdleme22cN  35147  cdleme22d  35148  cdleme22e  35149  cdleme22eALTN  35150  cdleme23b  35155  cdleme30a  35183  cdlemefrs29pre00  35200  cdlemefrs29bpre0  35201  cdlemefrs29cpre1  35203  cdleme32fva  35242  cdleme35b  35255  cdleme35d  35257  cdleme35e  35258  cdleme42a  35276  cdleme42ke  35290  cdlemeg46frv  35330  cdlemg2fv2  35405  cdlemg2m  35409  cdlemg10bALTN  35441  cdlemg12e  35452  cdlemg31d  35505  trlcoabs2N  35527  trlcolem  35531  trljco  35545  cdlemh2  35621  cdlemh  35622  cdlemi1  35623  cdlemk4  35639  cdlemk9  35644  cdlemk9bN  35645  cdlemkid2  35729  dia2dimlem1  35870  dia2dimlem2  35871  dia2dimlem3  35872  doca2N  35932  djajN  35943  cdlemn10  36012  dihvalcqat  36045  dih1  36092  dihglbcpreN  36106  dihmeetbclemN  36110  dihmeetlem7N  36116  dihjatc1  36117  djhlj  36207  djh01  36218  dihjatc  36223
  Copyright terms: Public domain W3C validator