![]() |
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 38724 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
2 | atllat 38664 | . 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Latclat 18388 AtLatcal 38628 HLchlt 38714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-dm 5677 df-iota 6486 df-fv 6542 df-ov 7405 df-atl 38662 df-cvlat 38686 df-hlat 38715 |
This theorem is referenced by: hllatd 38728 hlpos 38730 hlatjcl 38731 hlatjcom 38732 hlatjidm 38733 hlatjass 38734 hlatj32 38736 hlatj4 38738 hlatlej1 38739 atnlej1 38744 atnlej2 38745 hlateq 38764 hlrelat5N 38766 hlrelat2 38768 cvr2N 38776 cvrval5 38780 cvrexchlem 38784 cvrexch 38785 cvratlem 38786 cvrat 38787 cvrat2 38794 atcvrj2b 38797 atltcvr 38800 atlelt 38803 cvrat3 38807 cvrat4 38808 cvrat42 38809 2atjm 38810 3noncolr2 38814 3dimlem3OLDN 38827 3dimlem4OLDN 38830 1cvrat 38841 ps-1 38842 ps-2 38843 hlatexch3N 38845 3at 38855 llnneat 38879 lplni2 38902 2atnelpln 38909 lplnneat 38910 lplnnelln 38911 islpln2a 38913 2lplnmN 38924 2llnmj 38925 2llnm2N 38933 2llnm3N 38934 2llnm4 38935 2llnmeqat 38936 islvol5 38944 3atnelvolN 38951 lvolneatN 38953 lvolnelln 38954 lvolnelpln 38955 2lplnm2N 38986 2lplnmj 38987 pmap11 39127 isline3 39141 lncvrelatN 39146 2atm2atN 39150 2llnma1b 39151 2llnma3r 39153 paddasslem16 39200 paddass 39203 padd12N 39204 pmod2iN 39214 pmodN 39215 pmapjat1 39218 pmapjat2 39219 pmapjlln1 39220 hlmod1i 39221 atmod2i1 39226 atmod2i2 39227 atmod3i1 39229 atmod3i2 39230 atmod4i1 39231 atmod4i2 39232 llnexch2N 39235 polsubN 39272 paddunN 39292 pmapj2N 39294 pmapocjN 39295 psubclinN 39313 paddatclN 39314 linepsubclN 39316 lhpocnle 39381 lhpjat2 39386 lhpmcvr 39388 lhpm0atN 39394 lhpmatb 39396 trlval2 39528 trlcl 39529 trlle 39549 cdlemd1 39563 cdleme0cp 39579 cdleme0cq 39580 cdleme1b 39591 cdleme1 39592 cdleme2 39593 cdleme3b 39594 cdleme3c 39595 cdleme3e 39597 cdleme9b 39617 cdlemedb 39662 cdleme20zN 39666 cdleme19a 39668 cdlemf2 39927 tendoidcl 40134 dia1eldmN 40406 dialss 40411 dia1N 40418 diaglbN 40420 diaintclN 40423 docaclN 40489 doca2N 40491 djajN 40502 dibglbN 40531 dibintclN 40532 dihlsscpre 40599 dih2dimbALTN 40610 dih1 40651 dihglblem5apreN 40656 dihglblem5aN 40657 dihglblem2aN 40658 dihmeetcl 40710 dochvalr 40722 djhlj 40766 |
Copyright terms: Public domain | W3C validator |