Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlomcmcv Structured version   Visualization version   GIF version

Theorem hlomcmcv 37133
Description: A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
hlomcmcv (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))

Proof of Theorem hlomcmcv
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2738 . . 3 (le‘𝐾) = (le‘𝐾)
3 eqid 2738 . . 3 (lt‘𝐾) = (lt‘𝐾)
4 eqid 2738 . . 3 (join‘𝐾) = (join‘𝐾)
5 eqid 2738 . . 3 (0.‘𝐾) = (0.‘𝐾)
6 eqid 2738 . . 3 (1.‘𝐾) = (1.‘𝐾)
7 eqid 2738 . . 3 (Atoms‘𝐾) = (Atoms‘𝐾)
81, 2, 3, 4, 5, 6, 7ishlat1 37129 . 2 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ (Atoms‘𝐾)∀𝑦 ∈ (Atoms‘𝐾)(𝑥𝑦 → ∃𝑧 ∈ (Atoms‘𝐾)(𝑧𝑥𝑧𝑦𝑧(le‘𝐾)(𝑥(join‘𝐾)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝐾)∃𝑦 ∈ (Base‘𝐾)∃𝑧 ∈ (Base‘𝐾)(((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))))
98simplbi 501 1 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089  wcel 2111  wne 2941  wral 3062  wrex 3063   class class class wbr 5067  cfv 6397  (class class class)co 7231  Basecbs 16784  lecple 16833  ltcplt 17839  joincjn 17842  0.cp0 17953  1.cp1 17954  CLatccla 18028  OMLcoml 36952  Atomscatm 37040  CvLatclc 37042  HLchlt 37127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-iota 6355  df-fv 6405  df-ov 7234  df-hlat 37128
This theorem is referenced by:  hloml  37134  hlclat  37135  hlcvl  37136  cvr1  37187  cvrp  37193  atcvr1  37194  atcvr2  37195
  Copyright terms: Public domain W3C validator