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

Theorem hlexch1 36510
Description: A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.)
Hypotheses
Ref Expression
hlsuprexch.b 𝐵 = (Base‘𝐾)
hlsuprexch.l = (le‘𝐾)
hlsuprexch.j = (join‘𝐾)
hlsuprexch.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
hlexch1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))

Proof of Theorem hlexch1
StepHypRef Expression
1 hlcvl 36487 . 2 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
2 hlsuprexch.b . . 3 𝐵 = (Base‘𝐾)
3 hlsuprexch.l . . 3 = (le‘𝐾)
4 hlsuprexch.j . . 3 = (join‘𝐾)
5 hlsuprexch.a . . 3 𝐴 = (Atoms‘𝐾)
62, 3, 4, 5cvlexch1 36456 . 2 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))
71, 6syl3an1 1157 1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  w3a 1081   = wceq 1530  wcel 2107   class class class wbr 5057  cfv 6348  (class class class)co 7148  Basecbs 16475  lecple 16564  joincjn 17546  Atomscatm 36391  CvLatclc 36393  HLchlt 36478
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-cvlat 36450  df-hlat 36479
This theorem is referenced by:  cvratlem  36549  4noncolr3  36581  3dimlem4a  36591  3dimlem4OLDN  36593  ps-2  36606  4atlem0a  36721
  Copyright terms: Public domain W3C validator