Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlol | Structured version Visualization version GIF version |
Description: A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hlol | ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hloml 37134 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | |
2 | omlol 37017 | . 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 OLcol 36951 OMLcoml 36952 HLchlt 37127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-rex 3068 df-rab 3071 df-v 3422 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-nul 4252 df-if 4454 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4834 df-br 5068 df-iota 6355 df-fv 6405 df-ov 7234 df-oml 36956 df-hlat 37128 |
This theorem is referenced by: hlop 37139 cvrexch 37197 atle 37213 athgt 37233 2at0mat0 37302 dalem24 37474 pmapjat1 37630 atmod1i1m 37635 llnexchb2lem 37645 dalawlem2 37649 dalawlem6 37653 dalawlem7 37654 dalawlem11 37658 dalawlem12 37659 poldmj1N 37705 pmapj2N 37706 2polatN 37709 lhpmcvr3 37802 lhp2at0 37809 lhp2at0nle 37812 lhpelim 37814 lhpmod2i2 37815 lhpmod6i1 37816 lhprelat3N 37817 lhple 37819 4atex2-0aOLDN 37855 trljat1 37943 trljat2 37944 cdlemc1 37968 cdlemc6 37973 cdleme0cp 37991 cdleme0cq 37992 cdleme0e 37994 cdleme1 38004 cdleme2 38005 cdleme3c 38007 cdleme4 38015 cdleme5 38017 cdleme7c 38022 cdleme7e 38024 cdleme8 38027 cdleme9 38030 cdleme10 38031 cdleme15b 38052 cdlemednpq 38076 cdleme20c 38088 cdleme20d 38089 cdleme20j 38095 cdleme22cN 38119 cdleme22d 38120 cdleme22e 38121 cdleme22eALTN 38122 cdleme23b 38127 cdleme30a 38155 cdlemefrs29pre00 38172 cdlemefrs29bpre0 38173 cdlemefrs29cpre1 38175 cdleme32fva 38214 cdleme35b 38227 cdleme35d 38229 cdleme35e 38230 cdleme42a 38248 cdleme42ke 38262 cdlemeg46frv 38302 cdlemg2fv2 38377 cdlemg2m 38381 cdlemg10bALTN 38413 cdlemg12e 38424 cdlemg31d 38477 trlcoabs2N 38499 trlcolem 38503 trljco 38517 cdlemh2 38593 cdlemh 38594 cdlemi1 38595 cdlemk4 38611 cdlemk9 38616 cdlemk9bN 38617 cdlemkid2 38701 dia2dimlem1 38841 dia2dimlem2 38842 dia2dimlem3 38843 doca2N 38903 djajN 38914 cdlemn10 38983 dihvalcqat 39016 dih1 39063 dihglbcpreN 39077 dihmeetbclemN 39081 dihmeetlem7N 39087 dihjatc1 39088 djhlj 39178 djh01 39189 dihjatc 39194 |
Copyright terms: Public domain | W3C validator |