![]() |
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 35935 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | |
2 | omlol 35818 | . 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 OLcol 35752 OMLcoml 35753 HLchlt 35928 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-iota 6152 df-fv 6196 df-ov 6979 df-oml 35757 df-hlat 35929 |
This theorem is referenced by: hlop 35940 cvrexch 35998 atle 36014 athgt 36034 2at0mat0 36103 dalem24 36275 pmapjat1 36431 atmod1i1m 36436 llnexchb2lem 36446 dalawlem2 36450 dalawlem6 36454 dalawlem7 36455 dalawlem11 36459 dalawlem12 36460 poldmj1N 36506 pmapj2N 36507 2polatN 36510 lhpmcvr3 36603 lhp2at0 36610 lhp2at0nle 36613 lhpelim 36615 lhpmod2i2 36616 lhpmod6i1 36617 lhprelat3N 36618 lhple 36620 4atex2-0aOLDN 36656 trljat1 36744 trljat2 36745 cdlemc1 36769 cdlemc6 36774 cdleme0cp 36792 cdleme0cq 36793 cdleme0e 36795 cdleme1 36805 cdleme2 36806 cdleme3c 36808 cdleme4 36816 cdleme5 36818 cdleme7c 36823 cdleme7e 36825 cdleme8 36828 cdleme9 36831 cdleme10 36832 cdleme15b 36853 cdlemednpq 36877 cdleme20c 36889 cdleme20d 36890 cdleme20j 36896 cdleme22cN 36920 cdleme22d 36921 cdleme22e 36922 cdleme22eALTN 36923 cdleme23b 36928 cdleme30a 36956 cdlemefrs29pre00 36973 cdlemefrs29bpre0 36974 cdlemefrs29cpre1 36976 cdleme32fva 37015 cdleme35b 37028 cdleme35d 37030 cdleme35e 37031 cdleme42a 37049 cdleme42ke 37063 cdlemeg46frv 37103 cdlemg2fv2 37178 cdlemg2m 37182 cdlemg10bALTN 37214 cdlemg12e 37225 cdlemg31d 37278 trlcoabs2N 37300 trlcolem 37304 trljco 37318 cdlemh2 37394 cdlemh 37395 cdlemi1 37396 cdlemk4 37412 cdlemk9 37417 cdlemk9bN 37418 cdlemkid2 37502 dia2dimlem1 37642 dia2dimlem2 37643 dia2dimlem3 37644 doca2N 37704 djajN 37715 cdlemn10 37784 dihvalcqat 37817 dih1 37864 dihglbcpreN 37878 dihmeetbclemN 37882 dihmeetlem7N 37888 dihjatc1 37889 djhlj 37979 djh01 37990 dihjatc 37995 |
Copyright terms: Public domain | W3C validator |