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 35995
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 2773 . . . . 5 (lt‘𝐾) = (lt‘𝐾)
4 hlsuprexch.j . . . . 5 = (join‘𝐾)
5 eqid 2773 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
6 eqid 2773 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
7 hlsuprexch.a . . . . 5 𝐴 = (Atoms‘𝐾)
81, 2, 3, 4, 5, 6, 7ishlat2 35967 . . . 4 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))))
9 simprl 759 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ∧ ∃𝑥𝐵𝑦𝐵𝑧𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧𝑧(lt‘𝐾)(1.‘𝐾))))) → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))))
108, 9sylbi 209 . . 3 (𝐾 ∈ HL → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))))
11 neeq1 3024 . . . . . 6 (𝑥 = 𝑃 → (𝑥𝑦𝑃𝑦))
12 neeq2 3025 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧𝑥𝑧𝑃))
13 oveq1 6982 . . . . . . . . 9 (𝑥 = 𝑃 → (𝑥 𝑦) = (𝑃 𝑦))
1413breq2d 4938 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧 (𝑥 𝑦) ↔ 𝑧 (𝑃 𝑦)))
1512, 143anbi13d 1418 . . . . . . 7 (𝑥 = 𝑃 → ((𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)) ↔ (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))))
1615rexbidv 3237 . . . . . 6 (𝑥 = 𝑃 → (∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦)) ↔ ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))))
1711, 16imbi12d 337 . . . . 5 (𝑥 = 𝑃 → ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ↔ (𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)))))
18 breq1 4929 . . . . . . . . 9 (𝑥 = 𝑃 → (𝑥 𝑧𝑃 𝑧))
1918notbid 310 . . . . . . . 8 (𝑥 = 𝑃 → (¬ 𝑥 𝑧 ↔ ¬ 𝑃 𝑧))
20 breq1 4929 . . . . . . . 8 (𝑥 = 𝑃 → (𝑥 (𝑧 𝑦) ↔ 𝑃 (𝑧 𝑦)))
2119, 20anbi12d 622 . . . . . . 7 (𝑥 = 𝑃 → ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) ↔ (¬ 𝑃 𝑧𝑃 (𝑧 𝑦))))
22 oveq2 6983 . . . . . . . 8 (𝑥 = 𝑃 → (𝑧 𝑥) = (𝑧 𝑃))
2322breq2d 4938 . . . . . . 7 (𝑥 = 𝑃 → (𝑦 (𝑧 𝑥) ↔ 𝑦 (𝑧 𝑃)))
2421, 23imbi12d 337 . . . . . 6 (𝑥 = 𝑃 → (((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥)) ↔ ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))))
2524ralbidv 3142 . . . . 5 (𝑥 = 𝑃 → (∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥)) ↔ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))))
2617, 25anbi12d 622 . . . 4 (𝑥 = 𝑃 → (((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) ↔ ((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)))))
27 neeq2 3025 . . . . . 6 (𝑦 = 𝑄 → (𝑃𝑦𝑃𝑄))
28 neeq2 3025 . . . . . . . 8 (𝑦 = 𝑄 → (𝑧𝑦𝑧𝑄))
29 oveq2 6983 . . . . . . . . 9 (𝑦 = 𝑄 → (𝑃 𝑦) = (𝑃 𝑄))
3029breq2d 4938 . . . . . . . 8 (𝑦 = 𝑄 → (𝑧 (𝑃 𝑦) ↔ 𝑧 (𝑃 𝑄)))
3128, 303anbi23d 1419 . . . . . . 7 (𝑦 = 𝑄 → ((𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)) ↔ (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))))
3231rexbidv 3237 . . . . . 6 (𝑦 = 𝑄 → (∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦)) ↔ ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))))
3327, 32imbi12d 337 . . . . 5 (𝑦 = 𝑄 → ((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ↔ (𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄)))))
34 oveq2 6983 . . . . . . . . 9 (𝑦 = 𝑄 → (𝑧 𝑦) = (𝑧 𝑄))
3534breq2d 4938 . . . . . . . 8 (𝑦 = 𝑄 → (𝑃 (𝑧 𝑦) ↔ 𝑃 (𝑧 𝑄)))
3635anbi2d 620 . . . . . . 7 (𝑦 = 𝑄 → ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) ↔ (¬ 𝑃 𝑧𝑃 (𝑧 𝑄))))
37 breq1 4929 . . . . . . 7 (𝑦 = 𝑄 → (𝑦 (𝑧 𝑃) ↔ 𝑄 (𝑧 𝑃)))
3836, 37imbi12d 337 . . . . . 6 (𝑦 = 𝑄 → (((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)) ↔ ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
3938ralbidv 3142 . . . . 5 (𝑦 = 𝑄 → (∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃)) ↔ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
4033, 39anbi12d 622 . . . 4 (𝑦 = 𝑄 → (((𝑃𝑦 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑦𝑧 (𝑃 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑦)) → 𝑦 (𝑧 𝑃))) ↔ ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃)))))
4126, 40rspc2v 3543 . . 3 ((𝑃𝐴𝑄𝐴) → (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ∃𝑧𝐴 (𝑧𝑥𝑧𝑦𝑧 (𝑥 𝑦))) ∧ ∀𝑧𝐵 ((¬ 𝑥 𝑧𝑥 (𝑧 𝑦)) → 𝑦 (𝑧 𝑥))) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃)))))
4210, 41mpan9 499 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴)) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
43423impb 1096 1 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → ((𝑃𝑄 → ∃𝑧𝐴 (𝑧𝑃𝑧𝑄𝑧 (𝑃 𝑄))) ∧ ∀𝑧𝐵 ((¬ 𝑃 𝑧𝑃 (𝑧 𝑄)) → 𝑄 (𝑧 𝑃))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2962  wral 3083  wrex 3084   class class class wbr 4926  cfv 6186  (class class class)co 6975  Basecbs 16338  lecple 16427  ltcplt 17422  joincjn 17425  0.cp0 17518  1.cp1 17519  CLatccla 17588  OMLcoml 35789  Atomscatm 35877  AtLatcal 35878  HLchlt 35964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-iota 6150  df-fv 6194  df-ov 6978  df-cvlat 35936  df-hlat 35965
This theorem is referenced by:  hlsupr  36000
  Copyright terms: Public domain W3C validator