Theorem hlsuprexch

Description: A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011)

	Ref	Expression
Hypotheses	hlsuprexch.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlsuprexch.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlsuprexch.j	⊢ ∨ = ( join ‘ 𝐾 )
	hlsuprexch.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlsuprexch	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑄 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ ( 𝑧 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑧 ∨ 𝑃 ) ) ) )

Proof

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