Theorem hlsuprexch 39360

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.

Step	Hyp	Ref	Expression
1		hlsuprexch.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		hlsuprexch.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
3		eqid 2729	. . . . 5 ⊢ (lt‘𝐾) = (lt‘𝐾)
4		hlsuprexch.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
5		eqid 2729	. . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾)
6		eqid 2729	. . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾)
7		hlsuprexch.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	ishlat2 39331	. . . 4 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))))
9		simprl 770	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (((0.‘𝐾)(lt‘𝐾)𝑥 ∧ 𝑥(lt‘𝐾)𝑦) ∧ (𝑦(lt‘𝐾)𝑧 ∧ 𝑧(lt‘𝐾)(1.‘𝐾))))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
10	8, 9	sylbi 217	. . 3 ⊢ (𝐾 ∈ HL → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
11		neeq1 2987	. . . . . 6 ⊢ (𝑥 = 𝑃 → (𝑥 ≠ 𝑦 ↔ 𝑃 ≠ 𝑦))
12		neeq2 2988	. . . . . . . 8 ⊢ (𝑥 = 𝑃 → (𝑧 ≠ 𝑥 ↔ 𝑧 ≠ 𝑃))
13		oveq1 7360	. . . . . . . . 9 ⊢ (𝑥 = 𝑃 → (𝑥 ∨ 𝑦) = (𝑃 ∨ 𝑦))
14	13	breq2d 5107	. . . . . . . 8 ⊢ (𝑥 = 𝑃 → (𝑧 ≤ (𝑥 ∨ 𝑦) ↔ 𝑧 ≤ (𝑃 ∨ 𝑦)))
15	12, 14	3anbi13d 1440	. . . . . . 7 ⊢ (𝑥 = 𝑃 → ((𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ↔ (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦))))
16	15	rexbidv 3153	. . . . . 6 ⊢ (𝑥 = 𝑃 → (∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ↔ ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦))))
17	11, 16	imbi12d 344	. . . . 5 ⊢ (𝑥 = 𝑃 → ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ↔ (𝑃 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦)))))
18		breq1 5098	. . . . . . . . 9 ⊢ (𝑥 = 𝑃 → (𝑥 ≤ 𝑧 ↔ 𝑃 ≤ 𝑧))
19	18	notbid 318	. . . . . . . 8 ⊢ (𝑥 = 𝑃 → (¬ 𝑥 ≤ 𝑧 ↔ ¬ 𝑃 ≤ 𝑧))
20		breq1 5098	. . . . . . . 8 ⊢ (𝑥 = 𝑃 → (𝑥 ≤ (𝑧 ∨ 𝑦) ↔ 𝑃 ≤ (𝑧 ∨ 𝑦)))
21	19, 20	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = 𝑃 → ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) ↔ (¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦))))
22		oveq2 7361	. . . . . . . 8 ⊢ (𝑥 = 𝑃 → (𝑧 ∨ 𝑥) = (𝑧 ∨ 𝑃))
23	22	breq2d 5107	. . . . . . 7 ⊢ (𝑥 = 𝑃 → (𝑦 ≤ (𝑧 ∨ 𝑥) ↔ 𝑦 ≤ (𝑧 ∨ 𝑃)))
24	21, 23	imbi12d 344	. . . . . 6 ⊢ (𝑥 = 𝑃 → (((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ↔ ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃))))
25	24	ralbidv 3152	. . . . 5 ⊢ (𝑥 = 𝑃 → (∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ↔ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃))))
26	17, 25	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝑃 → (((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ↔ ((𝑃 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃)))))
27		neeq2 2988	. . . . . 6 ⊢ (𝑦 = 𝑄 → (𝑃 ≠ 𝑦 ↔ 𝑃 ≠ 𝑄))
28		neeq2 2988	. . . . . . . 8 ⊢ (𝑦 = 𝑄 → (𝑧 ≠ 𝑦 ↔ 𝑧 ≠ 𝑄))
29		oveq2 7361	. . . . . . . . 9 ⊢ (𝑦 = 𝑄 → (𝑃 ∨ 𝑦) = (𝑃 ∨ 𝑄))
30	29	breq2d 5107	. . . . . . . 8 ⊢ (𝑦 = 𝑄 → (𝑧 ≤ (𝑃 ∨ 𝑦) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
31	28, 30	3anbi23d 1441	. . . . . . 7 ⊢ (𝑦 = 𝑄 → ((𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦)) ↔ (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))))
32	31	rexbidv 3153	. . . . . 6 ⊢ (𝑦 = 𝑄 → (∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦)) ↔ ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))))
33	27, 32	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑄 → ((𝑃 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦))) ↔ (𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄)))))
34		oveq2 7361	. . . . . . . . 9 ⊢ (𝑦 = 𝑄 → (𝑧 ∨ 𝑦) = (𝑧 ∨ 𝑄))
35	34	breq2d 5107	. . . . . . . 8 ⊢ (𝑦 = 𝑄 → (𝑃 ≤ (𝑧 ∨ 𝑦) ↔ 𝑃 ≤ (𝑧 ∨ 𝑄)))
36	35	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = 𝑄 → ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) ↔ (¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄))))
37		breq1 5098	. . . . . . 7 ⊢ (𝑦 = 𝑄 → (𝑦 ≤ (𝑧 ∨ 𝑃) ↔ 𝑄 ≤ (𝑧 ∨ 𝑃)))
38	36, 37	imbi12d 344	. . . . . 6 ⊢ (𝑦 = 𝑄 → (((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃)) ↔ ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))
39	38	ralbidv 3152	. . . . 5 ⊢ (𝑦 = 𝑄 → (∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃)) ↔ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))
40	33, 39	anbi12d 632	. . . 4 ⊢ (𝑦 = 𝑄 → (((𝑃 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑃 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑃))) ↔ ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃)))))
41	26, 40	rspc2v 3590	. . 3 ⊢ ((𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃)))))
42	10, 41	mpan9 506	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))
43	42	3impb 1114	1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053   class class class wbr 5095  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  lecple 17186  ltcplt 18232  joincjn 18235  0.cp0 18345  1.cp1 18346  CLatccla 18422  OMLcoml 39153  Atomscatm 39241  AtLatcal 39242  HLchlt 39328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-cvlat 39300  df-hlat 39329

This theorem is referenced by:  hlsupr  39365