![]() |
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 35974 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
2 | atllat 35914 | . 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2051 Latclat 17526 AtLatcal 35878 HLchlt 35964 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-dm 5414 df-iota 6150 df-fv 6194 df-ov 6978 df-atl 35912 df-cvlat 35936 df-hlat 35965 |
This theorem is referenced by: hllatd 35978 hlpos 35980 hlatjcl 35981 hlatjcom 35982 hlatjidm 35983 hlatjass 35984 hlatj32 35986 hlatj4 35988 hlatlej1 35989 atnlej1 35993 atnlej2 35994 hlateq 36013 hlrelat5N 36015 hlrelat2 36017 cvr2N 36025 cvrval5 36029 cvrexchlem 36033 cvrexch 36034 cvratlem 36035 cvrat 36036 cvrat2 36043 atcvrj2b 36046 atltcvr 36049 atlelt 36052 cvrat3 36056 cvrat4 36057 cvrat42 36058 2atjm 36059 3noncolr2 36063 3dimlem3OLDN 36076 3dimlem4OLDN 36079 1cvrat 36090 ps-1 36091 ps-2 36092 hlatexch3N 36094 3at 36104 llnneat 36128 lplni2 36151 2atnelpln 36158 lplnneat 36159 lplnnelln 36160 islpln2a 36162 2lplnmN 36173 2llnmj 36174 2llnm2N 36182 2llnm3N 36183 2llnm4 36184 2llnmeqat 36185 islvol5 36193 3atnelvolN 36200 lvolneatN 36202 lvolnelln 36203 lvolnelpln 36204 2lplnm2N 36235 2lplnmj 36236 pmap11 36376 isline3 36390 lncvrelatN 36395 2atm2atN 36399 2llnma1b 36400 2llnma3r 36402 paddasslem16 36449 paddass 36452 padd12N 36453 pmod2iN 36463 pmodN 36464 pmapjat1 36467 pmapjat2 36468 pmapjlln1 36469 hlmod1i 36470 atmod2i1 36475 atmod2i2 36476 atmod3i1 36478 atmod3i2 36479 atmod4i1 36480 atmod4i2 36481 llnexch2N 36484 polsubN 36521 paddunN 36541 pmapj2N 36543 pmapocjN 36544 psubclinN 36562 paddatclN 36563 linepsubclN 36565 lhpocnle 36630 lhpjat2 36635 lhpmcvr 36637 lhpm0atN 36643 lhpmatb 36645 trlval2 36777 trlcl 36778 trlle 36798 cdlemd1 36812 cdleme0cp 36828 cdleme0cq 36829 cdleme1b 36840 cdleme1 36841 cdleme2 36842 cdleme3b 36843 cdleme3c 36844 cdleme3e 36846 cdleme9b 36866 cdlemedb 36911 cdleme20zN 36915 cdleme19a 36917 cdlemf2 37176 tendoidcl 37383 dia1eldmN 37655 dialss 37660 dia1N 37667 diaglbN 37669 diaintclN 37672 docaclN 37738 doca2N 37740 djajN 37751 dibglbN 37780 dibintclN 37781 dihlsscpre 37848 dih2dimbALTN 37859 dih1 37900 dihglblem5apreN 37905 dihglblem5aN 37906 dihglblem2aN 37907 dihmeetcl 37959 dochvalr 37971 djhlj 38015 |
Copyright terms: Public domain | W3C validator |