This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑄 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ ( 𝑧 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑧 ∨ 𝑃 ) ) ) )