| 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 39361 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
| 2 | atllat 39301 | . 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Latclat 18476 AtLatcal 39265 HLchlt 39351 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-dm 5695 df-iota 6514 df-fv 6569 df-ov 7434 df-atl 39299 df-cvlat 39323 df-hlat 39352 |
| This theorem is referenced by: hllatd 39365 hlpos 39367 hlatjcl 39368 hlatjcom 39369 hlatjidm 39370 hlatjass 39371 hlatj32 39373 hlatj4 39375 hlatlej1 39376 atnlej1 39381 atnlej2 39382 hlateq 39401 hlrelat5N 39403 hlrelat2 39405 cvr2N 39413 cvrval5 39417 cvrexchlem 39421 cvrexch 39422 cvratlem 39423 cvrat 39424 cvrat2 39431 atcvrj2b 39434 atltcvr 39437 atlelt 39440 cvrat3 39444 cvrat4 39445 cvrat42 39446 2atjm 39447 3noncolr2 39451 3dimlem3OLDN 39464 3dimlem4OLDN 39467 1cvrat 39478 ps-1 39479 ps-2 39480 hlatexch3N 39482 3at 39492 llnneat 39516 lplni2 39539 2atnelpln 39546 lplnneat 39547 lplnnelln 39548 islpln2a 39550 2lplnmN 39561 2llnmj 39562 2llnm2N 39570 2llnm3N 39571 2llnm4 39572 2llnmeqat 39573 islvol5 39581 3atnelvolN 39588 lvolneatN 39590 lvolnelln 39591 lvolnelpln 39592 2lplnm2N 39623 2lplnmj 39624 pmap11 39764 isline3 39778 lncvrelatN 39783 2atm2atN 39787 2llnma1b 39788 2llnma3r 39790 paddasslem16 39837 paddass 39840 padd12N 39841 pmod2iN 39851 pmodN 39852 pmapjat1 39855 pmapjat2 39856 pmapjlln1 39857 hlmod1i 39858 atmod2i1 39863 atmod2i2 39864 atmod3i1 39866 atmod3i2 39867 atmod4i1 39868 atmod4i2 39869 llnexch2N 39872 polsubN 39909 paddunN 39929 pmapj2N 39931 pmapocjN 39932 psubclinN 39950 paddatclN 39951 linepsubclN 39953 lhpocnle 40018 lhpjat2 40023 lhpmcvr 40025 lhpm0atN 40031 lhpmatb 40033 trlval2 40165 trlcl 40166 trlle 40186 cdlemd1 40200 cdleme0cp 40216 cdleme0cq 40217 cdleme1b 40228 cdleme1 40229 cdleme2 40230 cdleme3b 40231 cdleme3c 40232 cdleme3e 40234 cdleme9b 40254 cdlemedb 40299 cdleme20zN 40303 cdleme19a 40305 cdlemf2 40564 tendoidcl 40771 dia1eldmN 41043 dialss 41048 dia1N 41055 diaglbN 41057 diaintclN 41060 docaclN 41126 doca2N 41128 djajN 41139 dibglbN 41168 dibintclN 41169 dihlsscpre 41236 dih2dimbALTN 41247 dih1 41288 dihglblem5apreN 41293 dihglblem5aN 41294 dihglblem2aN 41295 dihmeetcl 41347 dochvalr 41359 djhlj 41403 |
| Copyright terms: Public domain | W3C validator |