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

Theorem hllat 30223
Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hllat  |-  ( K  e.  HL  ->  K  e.  Lat )

Proof of Theorem hllat
StepHypRef Expression
1 hlatl 30220 . 2  |-  ( K  e.  HL  ->  K  e.  AtLat )
2 atllat 30160 . 2  |-  ( K  e.  AtLat  ->  K  e.  Lat )
31, 2syl 16 1  |-  ( K  e.  HL  ->  K  e.  Lat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   Latclat 14476   AtLatcal 30124   HLchlt 30210
This theorem is referenced by:  hlpos  30225  hlatjcl  30226  hlatjcom  30227  hlatjidm  30228  hlatjass  30229  hlatj32  30231  hlatj4  30233  hlatlej1  30234  atnlej1  30238  atnlej2  30239  hlateq  30258  hlrelat5N  30260  hlrelat  30261  hlrelat2  30262  exatleN  30263  intnatN  30266  cvr2N  30270  hlrelat3  30271  cvrval3  30272  cvrval5  30274  cvrexchlem  30278  cvrexch  30279  cvratlem  30280  cvrat  30281  lnnat  30286  cvrat2  30288  atcvrj2b  30291  atltcvr  30294  atlelt  30297  2atlt  30298  atexchcvrN  30299  cvrat3  30301  cvrat4  30302  cvrat42  30303  2atjm  30304  atbtwn  30305  3noncolr2  30308  4noncolr3  30312  athgt  30315  3dim0  30316  3dimlem3a  30319  3dimlem3OLDN  30321  3dimlem4a  30322  3dimlem4OLDN  30324  3dim3  30328  1cvratex  30332  1cvrjat  30334  1cvrat  30335  ps-1  30336  ps-2  30337  hlatexch3N  30339  hlatexch4  30340  ps-2b  30341  3atlem1  30342  3atlem2  30343  3atlem4  30345  3atlem5  30346  3atlem6  30347  3at  30349  llnneat  30373  2llnmat  30383  2at0mat0  30384  2atm  30386  ps-2c  30387  lplni2  30396  llnmlplnN  30398  lplnle  30399  2atnelpln  30403  lplnneat  30404  lplnnelln  30405  islpln2a  30407  2lplnmN  30418  2llnmj  30419  2atmat  30420  lplnexllnN  30423  2llnjaN  30425  2llnm2N  30427  2llnm3N  30428  2llnm4  30429  2llnmeqat  30430  lvoli3  30436  islvol5  30438  lvoli2  30440  lvolnle3at  30441  3atnelvolN  30445  lvolneatN  30447  lvolnelln  30448  lvolnelpln  30449  islvol2aN  30451  4atlem3  30455  4atlem3a  30456  4atlem3b  30457  4atlem4a  30458  4atlem4b  30459  4atlem4c  30460  4atlem4d  30461  4atlem9  30462  4atlem10a  30463  4atlem10  30465  4atlem11a  30466  4atlem11b  30467  4atlem11  30468  4atlem12a  30469  4atlem12b  30470  4atlem12  30471  4at  30472  4at2  30473  lplncvrlvol2  30474  lplncvrlvol  30475  2lplnja  30478  2lplnm2N  30480  2lplnmj  30481  dalemkelat  30483  pmap11  30621  isline3  30635  lneq2at  30637  lncvrelatN  30640  lncmp  30642  2lnat  30643  2atm2atN  30644  2llnma1b  30645  2llnma3r  30647  cdlema1N  30650  cdlemblem  30652  cdlemb  30653  paddasslem2  30680  paddasslem5  30683  paddasslem8  30686  paddasslem12  30690  paddasslem13  30691  paddasslem15  30693  paddasslem16  30694  paddass  30697  padd12N  30698  pmodlem1  30705  pmodlem2  30706  pmod2iN  30708  pmodN  30709  pmapjat1  30712  pmapjat2  30713  pmapjlln1  30714  hlmod1i  30715  atmod1i1m  30717  llnmod1i2  30719  atmod2i1  30720  atmod2i2  30721  llnmod2i2  30722  atmod3i1  30723  atmod3i2  30724  atmod4i1  30725  atmod4i2  30726  llnexchb2lem  30727  llnexchb2  30728  llnexch2N  30729  dalawlem1  30730  dalawlem2  30731  dalawlem3  30732  dalawlem4  30733  dalawlem5  30734  dalawlem6  30735  dalawlem7  30736  dalawlem8  30737  dalawlem9  30738  dalawlem11  30740  dalawlem12  30741  dalawlem15  30744  polsubN  30766  paddunN  30786  pmapj2N  30788  pmapocjN  30789  psubclinN  30807  paddatclN  30808  pclfinclN  30809  linepsubclN  30810  poml4N  30812  osumcllem5N  30819  osumcllem7N  30821  pexmidlem2N  30830  pexmidlem4N  30832  pl42lem1N  30838  pl42lem2N  30839  pl42lem4N  30841  pl42N  30842  lhp2lt  30860  lhpexle2lem  30868  lhpexle3lem  30870  lhpocnle  30875  lhpjat2  30880  lhpj1  30881  lhpmcvr  30882  lhpmcvr3  30884  lhpmcvr4N  30885  lhpmcvr5N  30886  lhpmcvr6N  30887  lhpm0atN  30888  lhpmatb  30890  lhp2at0  30891  lhp2atnle  30892  lhpelim  30896  lhpmod2i2  30897  lhpmod6i1  30898  lhprelat3N  30899  lhple  30901  lhpat3  30905  4atexlemkl  30916  ltrnm  30990  ltrnj  30991  ltrnel  30998  ltrncnvel  31001  ltrnmw  31010  trlval2  31022  trlcl  31023  trljat1  31025  trljat2  31026  trlle  31043  trlval3  31046  arglem1N  31049  cdlemc1  31050  cdlemc2  31051  cdlemc4  31053  cdlemc5  31054  cdlemc6  31055  cdlemd1  31057  cdlemd2  31058  cdlemd3  31059  cdlemd4  31060  cdlemd7  31063  cdleme0aa  31069  cdleme0b  31071  cdleme0c  31072  cdleme0cp  31073  cdleme0cq  31074  cdleme0e  31076  cdleme0fN  31077  cdlemeulpq  31079  cdleme01N  31080  cdleme0ex1N  31082  cdleme1b  31085  cdleme1  31086  cdleme2  31087  cdleme3b  31088  cdleme3c  31089  cdleme3e  31091  cdleme3g  31093  cdleme3h  31094  cdleme3  31096  cdleme4a  31098  cdleme5  31099  cdleme7aa  31101  cdleme7c  31104  cdleme7d  31105  cdleme7e  31106  cdleme7ga  31107  cdleme7  31108  cdleme8  31109  cdleme9b  31111  cdleme9  31112  cdleme10  31113  cdleme11c  31120  cdleme11e  31122  cdleme11fN  31123  cdleme11g  31124  cdleme11k  31127  cdleme11  31129  cdleme13  31131  cdleme15b  31134  cdleme15d  31136  cdleme15  31137  cdleme16b  31138  cdleme16e  31141  cdleme16f  31142  cdleme17b  31146  cdleme17c  31147  cdleme22gb  31153  cdlemedb  31156  cdlemednpq  31158  cdleme20zN  31160  cdleme19a  31162  cdleme19b  31163  cdleme19c  31164  cdleme19e  31166  cdleme20aN  31168  cdleme20bN  31169  cdleme20c  31170  cdleme20d  31171  cdleme20e  31172  cdleme20j  31177  cdleme20k  31178  cdleme20l2  31180  cdleme20l  31181  cdleme20m  31182  cdleme21c  31186  cdleme21ct  31188  cdleme22aa  31198  cdleme22b  31200  cdleme22cN  31201  cdleme22d  31202  cdleme22e  31203  cdleme22eALTN  31204  cdleme22f  31205  cdleme22g  31207  cdleme23a  31208  cdleme23b  31209  cdleme23c  31210  cdleme27N  31228  cdleme28a  31229  cdleme28b  31230  cdleme29ex  31233  cdleme30a  31237  cdlemefr29exN  31261  cdleme32b  31301  cdleme32c  31302  cdleme32e  31304  cdleme35a  31307  cdleme35fnpq  31308  cdleme35b  31309  cdleme35c  31310  cdleme35d  31311  cdleme35f  31313  cdleme42c  31331  cdleme42e  31338  cdleme42h  31341  cdleme42i  31342  cdleme42mgN  31347  cdleme48bw  31361  cdlemeg46frv  31384  cdlemeg46vrg  31386  cdlemeg46rgv  31387  cdlemeg46req  31388  cdleme50eq  31400  cdlemf1  31420  cdlemf2  31421  trlord  31428  cdlemg2fv2  31459  cdlemg2m  31463  cdlemg7fvbwN  31466  cdlemg4c  31471  cdlemg4  31476  cdlemg6c  31479  cdlemg8b  31487  cdlemg10bALTN  31495  cdlemg10c  31498  cdlemg10  31500  cdlemg11b  31501  cdlemg12f  31507  cdlemg12g  31508  cdlemg12  31509  cdlemg13a  31510  cdlemg17a  31520  cdlemg17dALTN  31523  cdlemg17  31536  cdlemg18b  31538  cdlemg19a  31542  cdlemg19  31543  cdlemg27a  31551  cdlemg27b  31555  cdlemg31a  31556  cdlemg31b  31557  cdlemg33b0  31560  cdlemg33a  31565  cdlemg35  31572  trlcolem  31585  cdlemg42  31588  cdlemg44a  31590  cdlemg46  31594  trljco  31599  trljco2  31600  tendoidcl  31628  tendococl  31631  tendopltp  31639  cdlemh1  31674  cdlemh2  31675  cdlemi1  31677  cdlemi  31679  cdlemk3  31692  cdlemk4  31693  cdlemkvcl  31701  cdlemk10  31702  cdlemk7  31707  cdlemk11  31708  cdlemk12  31709  cdlemkole  31712  cdlemk14  31713  cdlemk15  31714  cdlemk1u  31718  cdlemk5u  31720  cdlemk7u  31729  cdlemk11u  31730  cdlemk12u  31731  cdlemk37  31773  cdlemk39  31775  cdlemkid1  31781  cdlemkid2  31783  cdlemk48  31809  cdlemk50  31811  cdlemk51  31812  cdlemk52  31813  cdlemk39u  31827  dia1eldmN  31901  dialss  31906  dia11N  31908  dia1N  31913  diaglbN  31915  diaintclN  31918  dia2dimlem1  31924  dia2dimlem2  31925  dia2dimlem3  31926  dia2dimlem10  31933  dia2dimlem12  31935  cdlemm10N  31978  docaclN  31984  doca2N  31986  djajN  31997  dib11N  32020  dibglbN  32026  dibintclN  32027  diblss  32030  cdlemn2  32055  cdlemn10  32066  dihjustlem  32076  dihord1  32078  dihord2a  32079  dihord2b  32080  dihord2cN  32081  dihord11b  32082  dihord11c  32084  dihord2pre  32085  dihord2pre2  32086  dihlsscpre  32094  dib2dim  32103  dih2dimb  32104  dih2dimbALTN  32105  dihvalcq2  32107  dihopelvalcpre  32108  dihord6apre  32116  dihord5b  32119  dihord6b  32120  dihord5apre  32122  dih11  32125  dih1  32146  dihwN  32149  dihmeetlem1N  32150  dihglblem5apreN  32151  dihglblem5aN  32152  dihglblem2aN  32153  dihglblem2N  32154  dihglblem3N  32155  dihmeetlem2N  32159  dihglbcpreN  32160  dihmeetbclemN  32164  dihmeetlem3N  32165  dihmeetlem4preN  32166  dihmeetlem6  32169  dihmeetlem7N  32170  dihjatc1  32171  dihjatc2N  32172  dihjatc3  32173  dihmeetlem9N  32175  dihmeetlem10N  32176  dihmeetlem11N  32177  dihmeetlem15N  32181  dihmeetlem16N  32182  dihmeetlem17N  32183  dihmeetlem19N  32185  dihmeetlem20N  32186  dihmeetALTN  32187  dihmeetcl  32205  dihmeet2  32206  dochvalr  32217  djhlj  32261  djhljjN  32262  djhj  32264  dihjatcclem1  32278  dihjatcclem2  32279  dihjatcclem4  32281  dihprrnlem1N  32284  dihprrnlem2  32285  dihjat6  32294  dihjat5N  32297  dvh4dimat  32298
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086  df-atl 30158  df-cvlat 30182  df-hlat 30211
  Copyright terms: Public domain W3C validator