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 37138
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 37134 . 2 (𝐾 ∈ HL → 𝐾 ∈ OML)
2 omlol 37017 . 2 (𝐾 ∈ OML → 𝐾 ∈ OL)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OL)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  OLcol 36951  OMLcoml 36952  HLchlt 37127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-iota 6355  df-fv 6405  df-ov 7234  df-oml 36956  df-hlat 37128
This theorem is referenced by:  hlop  37139  cvrexch  37197  atle  37213  athgt  37233  2at0mat0  37302  dalem24  37474  pmapjat1  37630  atmod1i1m  37635  llnexchb2lem  37645  dalawlem2  37649  dalawlem6  37653  dalawlem7  37654  dalawlem11  37658  dalawlem12  37659  poldmj1N  37705  pmapj2N  37706  2polatN  37709  lhpmcvr3  37802  lhp2at0  37809  lhp2at0nle  37812  lhpelim  37814  lhpmod2i2  37815  lhpmod6i1  37816  lhprelat3N  37817  lhple  37819  4atex2-0aOLDN  37855  trljat1  37943  trljat2  37944  cdlemc1  37968  cdlemc6  37973  cdleme0cp  37991  cdleme0cq  37992  cdleme0e  37994  cdleme1  38004  cdleme2  38005  cdleme3c  38007  cdleme4  38015  cdleme5  38017  cdleme7c  38022  cdleme7e  38024  cdleme8  38027  cdleme9  38030  cdleme10  38031  cdleme15b  38052  cdlemednpq  38076  cdleme20c  38088  cdleme20d  38089  cdleme20j  38095  cdleme22cN  38119  cdleme22d  38120  cdleme22e  38121  cdleme22eALTN  38122  cdleme23b  38127  cdleme30a  38155  cdlemefrs29pre00  38172  cdlemefrs29bpre0  38173  cdlemefrs29cpre1  38175  cdleme32fva  38214  cdleme35b  38227  cdleme35d  38229  cdleme35e  38230  cdleme42a  38248  cdleme42ke  38262  cdlemeg46frv  38302  cdlemg2fv2  38377  cdlemg2m  38381  cdlemg10bALTN  38413  cdlemg12e  38424  cdlemg31d  38477  trlcoabs2N  38499  trlcolem  38503  trljco  38517  cdlemh2  38593  cdlemh  38594  cdlemi1  38595  cdlemk4  38611  cdlemk9  38616  cdlemk9bN  38617  cdlemkid2  38701  dia2dimlem1  38841  dia2dimlem2  38842  dia2dimlem3  38843  doca2N  38903  djajN  38914  cdlemn10  38983  dihvalcqat  39016  dih1  39063  dihglbcpreN  39077  dihmeetbclemN  39081  dihmeetlem7N  39087  dihjatc1  39088  djhlj  39178  djh01  39189  dihjatc  39194
  Copyright terms: Public domain W3C validator