| 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 39358 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | |
| 2 | omlol 39241 | . 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 OLcol 39175 OMLcoml 39176 HLchlt 39351 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-oml 39180 df-hlat 39352 |
| This theorem is referenced by: hlop 39363 cvrexch 39422 atle 39438 athgt 39458 2at0mat0 39527 dalem24 39699 pmapjat1 39855 atmod1i1m 39860 llnexchb2lem 39870 dalawlem2 39874 dalawlem6 39878 dalawlem7 39879 dalawlem11 39883 dalawlem12 39884 poldmj1N 39930 pmapj2N 39931 2polatN 39934 lhpmcvr3 40027 lhp2at0 40034 lhp2at0nle 40037 lhpelim 40039 lhpmod2i2 40040 lhpmod6i1 40041 lhprelat3N 40042 lhple 40044 4atex2-0aOLDN 40080 trljat1 40168 trljat2 40169 cdlemc1 40193 cdlemc6 40198 cdleme0cp 40216 cdleme0cq 40217 cdleme0e 40219 cdleme1 40229 cdleme2 40230 cdleme3c 40232 cdleme4 40240 cdleme5 40242 cdleme7c 40247 cdleme7e 40249 cdleme8 40252 cdleme9 40255 cdleme10 40256 cdleme15b 40277 cdlemednpq 40301 cdleme20c 40313 cdleme20d 40314 cdleme20j 40320 cdleme22cN 40344 cdleme22d 40345 cdleme22e 40346 cdleme22eALTN 40347 cdleme23b 40352 cdleme30a 40380 cdlemefrs29pre00 40397 cdlemefrs29bpre0 40398 cdlemefrs29cpre1 40400 cdleme32fva 40439 cdleme35b 40452 cdleme35d 40454 cdleme35e 40455 cdleme42a 40473 cdleme42ke 40487 cdlemeg46frv 40527 cdlemg2fv2 40602 cdlemg2m 40606 cdlemg10bALTN 40638 cdlemg12e 40649 cdlemg31d 40702 trlcoabs2N 40724 trlcolem 40728 trljco 40742 cdlemh2 40818 cdlemh 40819 cdlemi1 40820 cdlemk4 40836 cdlemk9 40841 cdlemk9bN 40842 cdlemkid2 40926 dia2dimlem1 41066 dia2dimlem2 41067 dia2dimlem3 41068 doca2N 41128 djajN 41139 cdlemn10 41208 dihvalcqat 41241 dih1 41288 dihglbcpreN 41302 dihmeetbclemN 41306 dihmeetlem7N 41312 dihjatc1 41313 djhlj 41403 djh01 41414 dihjatc 41419 |
| Copyright terms: Public domain | W3C validator |