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

Theorem hlsuprexch 36397
Description: A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.)
Hypotheses
Ref Expression
hlsuprexch.b 𝐵 = (Base‘𝐾)
hlsuprexch.l = (le‘𝐾)
hlsuprexch.j = (join‘𝐾)
hlsuprexch.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
hlsuprexch ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝑧,𝐾   𝑧,𝑃   𝑧,𝑄
Allowed substitution hints:   (𝑧)   (𝑧)

Proof of Theorem hlsuprexch
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hlsuprexch.b . . . . 5 𝐵 = (Base‘𝐾)
2 hlsuprexch.l . . . . 5 = (le‘𝐾)
3 eqid 2818 . . . . 5 (lt‘𝐾) = (lt‘𝐾)
4 hlsuprexch.j . . . . 5 = (join‘𝐾)
5 eqid 2818 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
6 eqid 2818 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
7 hlsuprexch.a . . . . 5 𝐴 = (Atoms‘𝐾)
81, 2, 3, 4, 5, 6, 7ishlat2 36369 . . . 4 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))))
9 simprl 767 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))) → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))))
108, 9sylbi 218 . . 3 (𝐾 ∈ HL → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))))
11 neeq1 3075 . . . . . 6 (𝑥 = 𝑃 → (𝑥𝑦𝑃𝑦))
12 neeq2 3076 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧𝑥𝑧𝑃))
13 oveq1 7152 . . . . . . . . 9 (𝑥 = 𝑃 → (𝑥 𝑦) = (𝑃 𝑦))
1413breq2d 5069 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧 (𝑥 𝑦) ↔ 𝑧 (𝑃 𝑦)))
1512, 143anbi13d 1429 . . . . . . 7 (𝑥 = 𝑃 → ((𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)) ↔ (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))))
1615rexbidv 3294 . . . . . 6 (𝑥 = 𝑃 → (∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)) ↔ ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))))
1711, 16imbi12d 346 . . . . 5 (𝑥 = 𝑃 → ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ↔ (𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)))))
18 breq1 5060 . . . . . . . . 9 (𝑥 = 𝑃 → (𝑥 𝑧𝑃 𝑧))
1918notbid 319 . . . . . . . 8 (𝑥 = 𝑃 → (¬ 𝑥 𝑧 ↔ ¬ 𝑃 𝑧))
20 breq1 5060 . . . . . . . 8 (𝑥 = 𝑃 → (𝑥 (𝑧 𝑦) ↔ 𝑃 (𝑧 𝑦)))
2119, 20anbi12d 630 . . . . . . 7 (𝑥 = 𝑃 → ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) ↔ (¬ 𝑃 𝑧𝑃 (𝑧 𝑦))))
22 oveq2 7153 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧 𝑥) = (𝑧 𝑃))
2322breq2d 5069 . . . . . . 7 (𝑥 = 𝑃 → (𝑦 (𝑧 𝑥) ↔ 𝑦 (𝑧 𝑃)))
2421, 23imbi12d 346 . . . . . 6 (𝑥 = 𝑃 → (((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥)) ↔ ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))))
2524ralbidv 3194 . . . . 5 (𝑥 = 𝑃 → (∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥)) ↔ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))))
2617, 25anbi12d 630 . . . 4 (𝑥 = 𝑃 → (((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ↔ ((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)))))
27 neeq2 3076 . . . . . 6 (𝑦 = 𝑄 → (𝑃𝑦𝑃𝑄))
28 neeq2 3076 . . . . . . . 8 (𝑦 = 𝑄 → (𝑧𝑦𝑧𝑄))
29 oveq2 7153 . . . . . . . . 9 (𝑦 = 𝑄 → (𝑃 𝑦) = (𝑃 𝑄))
3029breq2d 5069 . . . . . . . 8 (𝑦 = 𝑄 → (𝑧 (𝑃 𝑦) ↔ 𝑧 (𝑃 𝑄)))
3128, 303anbi23d 1430 . . . . . . 7 (𝑦 = 𝑄 → ((𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)) ↔ (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))))
3231rexbidv 3294 . . . . . 6 (𝑦 = 𝑄 → (∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)) ↔ ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))))
3327, 32imbi12d 346 . . . . 5 (𝑦 = 𝑄 → ((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ↔ (𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄)))))
34 oveq2 7153 . . . . . . . . 9 (𝑦 = 𝑄 → (𝑧 𝑦) = (𝑧 𝑄))
3534breq2d 5069 . . . . . . . 8 (𝑦 = 𝑄 → (𝑃 (𝑧 𝑦) ↔ 𝑃 (𝑧 𝑄)))
3635anbi2d 628 . . . . . . 7 (𝑦 = 𝑄 → ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) ↔ (¬ 𝑃 𝑧𝑃 (𝑧 𝑄))))
37 breq1 5060 . . . . . . 7 (𝑦 = 𝑄 → (𝑦 (𝑧 𝑃) ↔ 𝑄 (𝑧 𝑃)))
3836, 37imbi12d 346 . . . . . 6 (𝑦 = 𝑄 → (((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)) ↔ ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
3938ralbidv 3194 . . . . 5 (𝑦 = 𝑄 → (∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)) ↔ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
4033, 39anbi12d 630 . . . 4 (𝑦 = 𝑄 → (((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))) ↔ ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃)))))
4126, 40rspc2v 3630 . . 3 ((𝑃𝐴𝑄𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃)))))
4210, 41mpan9 507 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴)) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
43423impb 1107 1 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136   class class class wbr 5057  cfv 6348  (class class class)co 7145  Basecbs 16471  lecple 16560  ltcplt 17539  joincjn 17542  0.cp0 17635  1.cp1 17636  CLatccla 17705  OMLcoml 36191  Atomscatm 36279  AtLatcal 36280  HLchlt 36366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-cvlat 36338  df-hlat 36367
This theorem is referenced by:  hlsupr  36402
  Copyright terms: Public domain W3C validator