![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlomcmcv | Structured version Visualization version GIF version |
Description: A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
Ref | Expression |
---|---|
hlomcmcv | ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . . 3 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
2 | eqid 2725 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | eqid 2725 | . . 3 ⊢ (lt‘𝐾) = (lt‘𝐾) | |
4 | eqid 2725 | . . 3 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | eqid 2725 | . . 3 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
6 | eqid 2725 | . . 3 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
7 | eqid 2725 | . . 3 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
8 | 1, 2, 3, 4, 5, 6, 7 | ishlat1 38954 | . 2 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ (Atoms‘𝐾)∀𝑦 ∈ (Atoms‘𝐾)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝐾)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝐾)(𝑥(join‘𝐾)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾)))))) |
9 | 8 | simplbi 496 | 1 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 ∈ wcel 2098 ≠ wne 2929 ∀wral 3050 ∃wrex 3059 class class class wbr 5149 ‘cfv 6549 (class class class)co 7419 Basecbs 17183 lecple 17243 ltcplt 18303 joincjn 18306 0.cp0 18418 1.cp1 18419 CLatccla 18493 OMLcoml 38777 Atomscatm 38865 CvLatclc 38867 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-hlat 38953 |
This theorem is referenced by: hloml 38959 hlclat 38960 hlcvl 38961 cvr1 39013 cvrp 39019 atcvr1 39020 atcvr2 39021 |
Copyright terms: Public domain | W3C validator |