![]() |
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 38959 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | |
2 | omlol 38842 | . 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 OLcol 38776 OMLcoml 38777 HLchlt 38952 |
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 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-oml 38781 df-hlat 38953 |
This theorem is referenced by: hlop 38964 cvrexch 39023 atle 39039 athgt 39059 2at0mat0 39128 dalem24 39300 pmapjat1 39456 atmod1i1m 39461 llnexchb2lem 39471 dalawlem2 39475 dalawlem6 39479 dalawlem7 39480 dalawlem11 39484 dalawlem12 39485 poldmj1N 39531 pmapj2N 39532 2polatN 39535 lhpmcvr3 39628 lhp2at0 39635 lhp2at0nle 39638 lhpelim 39640 lhpmod2i2 39641 lhpmod6i1 39642 lhprelat3N 39643 lhple 39645 4atex2-0aOLDN 39681 trljat1 39769 trljat2 39770 cdlemc1 39794 cdlemc6 39799 cdleme0cp 39817 cdleme0cq 39818 cdleme0e 39820 cdleme1 39830 cdleme2 39831 cdleme3c 39833 cdleme4 39841 cdleme5 39843 cdleme7c 39848 cdleme7e 39850 cdleme8 39853 cdleme9 39856 cdleme10 39857 cdleme15b 39878 cdlemednpq 39902 cdleme20c 39914 cdleme20d 39915 cdleme20j 39921 cdleme22cN 39945 cdleme22d 39946 cdleme22e 39947 cdleme22eALTN 39948 cdleme23b 39953 cdleme30a 39981 cdlemefrs29pre00 39998 cdlemefrs29bpre0 39999 cdlemefrs29cpre1 40001 cdleme32fva 40040 cdleme35b 40053 cdleme35d 40055 cdleme35e 40056 cdleme42a 40074 cdleme42ke 40088 cdlemeg46frv 40128 cdlemg2fv2 40203 cdlemg2m 40207 cdlemg10bALTN 40239 cdlemg12e 40250 cdlemg31d 40303 trlcoabs2N 40325 trlcolem 40329 trljco 40343 cdlemh2 40419 cdlemh 40420 cdlemi1 40421 cdlemk4 40437 cdlemk9 40442 cdlemk9bN 40443 cdlemkid2 40527 dia2dimlem1 40667 dia2dimlem2 40668 dia2dimlem3 40669 doca2N 40729 djajN 40740 cdlemn10 40809 dihvalcqat 40842 dih1 40889 dihglbcpreN 40903 dihmeetbclemN 40907 dihmeetlem7N 40913 dihjatc1 40914 djhlj 41004 djh01 41015 dihjatc 41020 |
Copyright terms: Public domain | W3C validator |