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 38765
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 2726 . . . . 5 (ltβ€˜πΎ) = (ltβ€˜πΎ)
4 hlsuprexch.j . . . . 5 ∨ = (joinβ€˜πΎ)
5 eqid 2726 . . . . 5 (0.β€˜πΎ) = (0.β€˜πΎ)
6 eqid 2726 . . . . 5 (1.β€˜πΎ) = (1.β€˜πΎ)
7 hlsuprexch.a . . . . 5 𝐴 = (Atomsβ€˜πΎ)
81, 2, 3, 4, 5, 6, 7ishlat2 38736 . . . 4 (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))) ∧ βˆƒπ‘₯ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (((0.β€˜πΎ)(ltβ€˜πΎ)π‘₯ ∧ π‘₯(ltβ€˜πΎ)𝑦) ∧ (𝑦(ltβ€˜πΎ)𝑧 ∧ 𝑧(ltβ€˜πΎ)(1.β€˜πΎ))))))
9 simprl 768 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))) ∧ βˆƒπ‘₯ ∈ 𝐡 βˆƒπ‘¦ ∈ 𝐡 βˆƒπ‘§ ∈ 𝐡 (((0.β€˜πΎ)(ltβ€˜πΎ)π‘₯ ∧ π‘₯(ltβ€˜πΎ)𝑦) ∧ (𝑦(ltβ€˜πΎ)𝑧 ∧ 𝑧(ltβ€˜πΎ)(1.β€˜πΎ))))) β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))))
108, 9sylbi 216 . . 3 (𝐾 ∈ HL β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))))
11 neeq1 2997 . . . . . 6 (π‘₯ = 𝑃 β†’ (π‘₯ β‰  𝑦 ↔ 𝑃 β‰  𝑦))
12 neeq2 2998 . . . . . . . 8 (π‘₯ = 𝑃 β†’ (𝑧 β‰  π‘₯ ↔ 𝑧 β‰  𝑃))
13 oveq1 7412 . . . . . . . . 9 (π‘₯ = 𝑃 β†’ (π‘₯ ∨ 𝑦) = (𝑃 ∨ 𝑦))
1413breq2d 5153 . . . . . . . 8 (π‘₯ = 𝑃 β†’ (𝑧 ≀ (π‘₯ ∨ 𝑦) ↔ 𝑧 ≀ (𝑃 ∨ 𝑦)))
1512, 143anbi13d 1434 . . . . . . 7 (π‘₯ = 𝑃 β†’ ((𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦)) ↔ (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦))))
1615rexbidv 3172 . . . . . 6 (π‘₯ = 𝑃 β†’ (βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦)) ↔ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦))))
1711, 16imbi12d 344 . . . . 5 (π‘₯ = 𝑃 β†’ ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ↔ (𝑃 β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦)))))
18 breq1 5144 . . . . . . . . 9 (π‘₯ = 𝑃 β†’ (π‘₯ ≀ 𝑧 ↔ 𝑃 ≀ 𝑧))
1918notbid 318 . . . . . . . 8 (π‘₯ = 𝑃 β†’ (Β¬ π‘₯ ≀ 𝑧 ↔ Β¬ 𝑃 ≀ 𝑧))
20 breq1 5144 . . . . . . . 8 (π‘₯ = 𝑃 β†’ (π‘₯ ≀ (𝑧 ∨ 𝑦) ↔ 𝑃 ≀ (𝑧 ∨ 𝑦)))
2119, 20anbi12d 630 . . . . . . 7 (π‘₯ = 𝑃 β†’ ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) ↔ (Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦))))
22 oveq2 7413 . . . . . . . 8 (π‘₯ = 𝑃 β†’ (𝑧 ∨ π‘₯) = (𝑧 ∨ 𝑃))
2322breq2d 5153 . . . . . . 7 (π‘₯ = 𝑃 β†’ (𝑦 ≀ (𝑧 ∨ π‘₯) ↔ 𝑦 ≀ (𝑧 ∨ 𝑃)))
2421, 23imbi12d 344 . . . . . 6 (π‘₯ = 𝑃 β†’ (((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯)) ↔ ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃))))
2524ralbidv 3171 . . . . 5 (π‘₯ = 𝑃 β†’ (βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯)) ↔ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃))))
2617, 25anbi12d 630 . . . 4 (π‘₯ = 𝑃 β†’ (((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))) ↔ ((𝑃 β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃)))))
27 neeq2 2998 . . . . . 6 (𝑦 = 𝑄 β†’ (𝑃 β‰  𝑦 ↔ 𝑃 β‰  𝑄))
28 neeq2 2998 . . . . . . . 8 (𝑦 = 𝑄 β†’ (𝑧 β‰  𝑦 ↔ 𝑧 β‰  𝑄))
29 oveq2 7413 . . . . . . . . 9 (𝑦 = 𝑄 β†’ (𝑃 ∨ 𝑦) = (𝑃 ∨ 𝑄))
3029breq2d 5153 . . . . . . . 8 (𝑦 = 𝑄 β†’ (𝑧 ≀ (𝑃 ∨ 𝑦) ↔ 𝑧 ≀ (𝑃 ∨ 𝑄)))
3128, 303anbi23d 1435 . . . . . . 7 (𝑦 = 𝑄 β†’ ((𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦)) ↔ (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))))
3231rexbidv 3172 . . . . . 6 (𝑦 = 𝑄 β†’ (βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦)) ↔ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))))
3327, 32imbi12d 344 . . . . 5 (𝑦 = 𝑄 β†’ ((𝑃 β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦))) ↔ (𝑃 β‰  𝑄 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄)))))
34 oveq2 7413 . . . . . . . . 9 (𝑦 = 𝑄 β†’ (𝑧 ∨ 𝑦) = (𝑧 ∨ 𝑄))
3534breq2d 5153 . . . . . . . 8 (𝑦 = 𝑄 β†’ (𝑃 ≀ (𝑧 ∨ 𝑦) ↔ 𝑃 ≀ (𝑧 ∨ 𝑄)))
3635anbi2d 628 . . . . . . 7 (𝑦 = 𝑄 β†’ ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) ↔ (Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄))))
37 breq1 5144 . . . . . . 7 (𝑦 = 𝑄 β†’ (𝑦 ≀ (𝑧 ∨ 𝑃) ↔ 𝑄 ≀ (𝑧 ∨ 𝑃)))
3836, 37imbi12d 344 . . . . . 6 (𝑦 = 𝑄 β†’ (((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃)) ↔ ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃))))
3938ralbidv 3171 . . . . 5 (𝑦 = 𝑄 β†’ (βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃)) ↔ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃))))
4033, 39anbi12d 630 . . . 4 (𝑦 = 𝑄 β†’ (((𝑃 β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (𝑃 ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ 𝑃))) ↔ ((𝑃 β‰  𝑄 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃)))))
4126, 40rspc2v 3617 . . 3 ((𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 ((π‘₯ β‰  𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  π‘₯ ∧ 𝑧 β‰  𝑦 ∧ 𝑧 ≀ (π‘₯ ∨ 𝑦))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ π‘₯ ≀ 𝑧 ∧ π‘₯ ≀ (𝑧 ∨ 𝑦)) β†’ 𝑦 ≀ (𝑧 ∨ π‘₯))) β†’ ((𝑃 β‰  𝑄 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃)))))
4210, 41mpan9 506 . 2 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) β†’ ((𝑃 β‰  𝑄 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃))))
43423impb 1112 1 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ ((𝑃 β‰  𝑄 β†’ βˆƒπ‘§ ∈ 𝐴 (𝑧 β‰  𝑃 ∧ 𝑧 β‰  𝑄 ∧ 𝑧 ≀ (𝑃 ∨ 𝑄))) ∧ βˆ€π‘§ ∈ 𝐡 ((Β¬ 𝑃 ≀ 𝑧 ∧ 𝑃 ≀ (𝑧 ∨ 𝑄)) β†’ 𝑄 ≀ (𝑧 ∨ 𝑃))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064   class class class wbr 5141  β€˜cfv 6537  (class class class)co 7405  Basecbs 17153  lecple 17213  ltcplt 18273  joincjn 18276  0.cp0 18388  1.cp1 18389  CLatccla 18463  OMLcoml 38558  Atomscatm 38646  AtLatcal 38647  HLchlt 38733
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 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6489  df-fv 6545  df-ov 7408  df-cvlat 38705  df-hlat 38734
This theorem is referenced by:  hlsupr  38770
  Copyright terms: Public domain W3C validator