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 34644 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | |
2 | omlol 34527 | . 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 OLcol 34461 OMLcoml 34462 HLchlt 34637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-oml 34466 df-hlat 34638 |
This theorem is referenced by: hlop 34649 cvrexch 34706 atle 34722 athgt 34742 2at0mat0 34811 dalem24 34983 pmapjat1 35139 atmod1i1m 35144 llnexchb2lem 35154 dalawlem2 35158 dalawlem6 35162 dalawlem7 35163 dalawlem11 35167 dalawlem12 35168 poldmj1N 35214 pmapj2N 35215 2polatN 35218 lhpmcvr3 35311 lhp2at0 35318 lhp2at0nle 35321 lhpelim 35323 lhpmod2i2 35324 lhpmod6i1 35325 lhprelat3N 35326 lhple 35328 4atex2-0aOLDN 35364 trljat1 35453 trljat2 35454 cdlemc1 35478 cdlemc6 35483 cdleme0cp 35501 cdleme0cq 35502 cdleme0e 35504 cdleme1 35514 cdleme2 35515 cdleme3c 35517 cdleme4 35525 cdleme5 35527 cdleme7c 35532 cdleme7e 35534 cdleme8 35537 cdleme9 35540 cdleme10 35541 cdleme15b 35562 cdlemednpq 35586 cdleme20yOLD 35590 cdleme20c 35599 cdleme20d 35600 cdleme20j 35606 cdleme22cN 35630 cdleme22d 35631 cdleme22e 35632 cdleme22eALTN 35633 cdleme23b 35638 cdleme30a 35666 cdlemefrs29pre00 35683 cdlemefrs29bpre0 35684 cdlemefrs29cpre1 35686 cdleme32fva 35725 cdleme35b 35738 cdleme35d 35740 cdleme35e 35741 cdleme42a 35759 cdleme42ke 35773 cdlemeg46frv 35813 cdlemg2fv2 35888 cdlemg2m 35892 cdlemg10bALTN 35924 cdlemg12e 35935 cdlemg31d 35988 trlcoabs2N 36010 trlcolem 36014 trljco 36028 cdlemh2 36104 cdlemh 36105 cdlemi1 36106 cdlemk4 36122 cdlemk9 36127 cdlemk9bN 36128 cdlemkid2 36212 dia2dimlem1 36353 dia2dimlem2 36354 dia2dimlem3 36355 doca2N 36415 djajN 36426 cdlemn10 36495 dihvalcqat 36528 dih1 36575 dihglbcpreN 36589 dihmeetbclemN 36593 dihmeetlem7N 36599 dihjatc1 36600 djhlj 36690 djh01 36701 dihjatc 36706 |
Copyright terms: Public domain | W3C validator |