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 35170
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 35166 . 2 (𝐾 ∈ HL → 𝐾 ∈ OML)
2 omlol 35049 . 2 (𝐾 ∈ OML → 𝐾 ∈ OL)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ OL)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2140  OLcol 34983  OMLcoml 34984  HLchlt 35159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-oml 34988  df-hlat 35160
This theorem is referenced by:  hlop  35171  cvrexch  35228  atle  35244  athgt  35264  2at0mat0  35333  dalem24  35505  pmapjat1  35661  atmod1i1m  35666  llnexchb2lem  35676  dalawlem2  35680  dalawlem6  35684  dalawlem7  35685  dalawlem11  35689  dalawlem12  35690  poldmj1N  35736  pmapj2N  35737  2polatN  35740  lhpmcvr3  35833  lhp2at0  35840  lhp2at0nle  35843  lhpelim  35845  lhpmod2i2  35846  lhpmod6i1  35847  lhprelat3N  35848  lhple  35850  4atex2-0aOLDN  35886  trljat1  35975  trljat2  35976  cdlemc1  36000  cdlemc6  36005  cdleme0cp  36023  cdleme0cq  36024  cdleme0e  36026  cdleme1  36036  cdleme2  36037  cdleme3c  36039  cdleme4  36047  cdleme5  36049  cdleme7c  36054  cdleme7e  36056  cdleme8  36059  cdleme9  36062  cdleme10  36063  cdleme15b  36084  cdlemednpq  36108  cdleme20c  36120  cdleme20d  36121  cdleme20j  36127  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22eALTN  36154  cdleme23b  36159  cdleme30a  36187  cdlemefrs29pre00  36204  cdlemefrs29bpre0  36205  cdlemefrs29cpre1  36207  cdleme32fva  36246  cdleme35b  36259  cdleme35d  36261  cdleme35e  36262  cdleme42a  36280  cdleme42ke  36294  cdlemeg46frv  36334  cdlemg2fv2  36409  cdlemg2m  36413  cdlemg10bALTN  36445  cdlemg12e  36456  cdlemg31d  36509  trlcoabs2N  36531  trlcolem  36535  trljco  36549  cdlemh2  36625  cdlemh  36626  cdlemi1  36627  cdlemk4  36643  cdlemk9  36648  cdlemk9bN  36649  cdlemkid2  36733  dia2dimlem1  36874  dia2dimlem2  36875  dia2dimlem3  36876  doca2N  36936  djajN  36947  cdlemn10  37016  dihvalcqat  37049  dih1  37096  dihglbcpreN  37110  dihmeetbclemN  37114  dihmeetlem7N  37120  dihjatc1  37121  djhlj  37211  djh01  37222  dihjatc  37227
  Copyright terms: Public domain W3C validator