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

Theorem hllat 36381
Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hllat (𝐾 ∈ HL → 𝐾 ∈ Lat)

Proof of Theorem hllat
StepHypRef Expression
1 hlatl 36378 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 36318 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Latclat 17645  AtLatcal 36282  HLchlt 36368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-dm 5559  df-iota 6308  df-fv 6357  df-ov 7148  df-atl 36316  df-cvlat 36340  df-hlat 36369
This theorem is referenced by:  hllatd  36382  hlpos  36384  hlatjcl  36385  hlatjcom  36386  hlatjidm  36387  hlatjass  36388  hlatj32  36390  hlatj4  36392  hlatlej1  36393  atnlej1  36397  atnlej2  36398  hlateq  36417  hlrelat5N  36419  hlrelat2  36421  cvr2N  36429  cvrval5  36433  cvrexchlem  36437  cvrexch  36438  cvratlem  36439  cvrat  36440  cvrat2  36447  atcvrj2b  36450  atltcvr  36453  atlelt  36456  cvrat3  36460  cvrat4  36461  cvrat42  36462  2atjm  36463  3noncolr2  36467  3dimlem3OLDN  36480  3dimlem4OLDN  36483  1cvrat  36494  ps-1  36495  ps-2  36496  hlatexch3N  36498  3at  36508  llnneat  36532  lplni2  36555  2atnelpln  36562  lplnneat  36563  lplnnelln  36564  islpln2a  36566  2lplnmN  36577  2llnmj  36578  2llnm2N  36586  2llnm3N  36587  2llnm4  36588  2llnmeqat  36589  islvol5  36597  3atnelvolN  36604  lvolneatN  36606  lvolnelln  36607  lvolnelpln  36608  2lplnm2N  36639  2lplnmj  36640  pmap11  36780  isline3  36794  lncvrelatN  36799  2atm2atN  36803  2llnma1b  36804  2llnma3r  36806  paddasslem16  36853  paddass  36856  padd12N  36857  pmod2iN  36867  pmodN  36868  pmapjat1  36871  pmapjat2  36872  pmapjlln1  36873  hlmod1i  36874  atmod2i1  36879  atmod2i2  36880  atmod3i1  36882  atmod3i2  36883  atmod4i1  36884  atmod4i2  36885  llnexch2N  36888  polsubN  36925  paddunN  36945  pmapj2N  36947  pmapocjN  36948  psubclinN  36966  paddatclN  36967  linepsubclN  36969  lhpocnle  37034  lhpjat2  37039  lhpmcvr  37041  lhpm0atN  37047  lhpmatb  37049  trlval2  37181  trlcl  37182  trlle  37202  cdlemd1  37216  cdleme0cp  37232  cdleme0cq  37233  cdleme1b  37244  cdleme1  37245  cdleme2  37246  cdleme3b  37247  cdleme3c  37248  cdleme3e  37250  cdleme9b  37270  cdlemedb  37315  cdleme20zN  37319  cdleme19a  37321  cdlemf2  37580  tendoidcl  37787  dia1eldmN  38059  dialss  38064  dia1N  38071  diaglbN  38073  diaintclN  38076  docaclN  38142  doca2N  38144  djajN  38155  dibglbN  38184  dibintclN  38185  dihlsscpre  38252  dih2dimbALTN  38263  dih1  38304  dihglblem5apreN  38309  dihglblem5aN  38310  dihglblem2aN  38311  dihmeetcl  38363  dochvalr  38375  djhlj  38419
  Copyright terms: Public domain W3C validator