Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hllat | Structured version Visualization version GIF version |
Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hllat | ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlatl 36378 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
2 | atllat 36318 | . 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) | |
3 | 1, 2 | syl 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 |