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

Metamath Proof Explorer

Theorem ishlatiN

Description: Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses ishlati.1 ⊢ 𝐾 ∈ OML
ishlati.2 ⊢ 𝐾 ∈ CLat
ishlati.3 ⊢ 𝐾 ∈ AtLat
ishlati.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ishlati.l ⊢ ≤ = ( le ‘ 𝐾 )
ishlati.s ⊢ < = ( lt ‘ 𝐾 )
ishlati.j ⊢ ∨ = ( join ‘ 𝐾 )
ishlati.z ⊢ 0 = ( 0. ‘ 𝐾 )
ishlati.u ⊢ 1 = ( 1. ‘ 𝐾 )
ishlati.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ishlati.9 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ ( 𝑧 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑧 ∨ 𝑥 ) ) )
ishlati.10 ⊢ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) )
Assertion ishlatiN 𝐾 ∈ HL

Proof

Step Hyp Ref Expression
1 ishlati.1 ⊢ 𝐾 ∈ OML
2 ishlati.2 ⊢ 𝐾 ∈ CLat
3 ishlati.3 ⊢ 𝐾 ∈ AtLat
4 ishlati.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
5 ishlati.l ⊢ ≤ = ( le ‘ 𝐾 )
6 ishlati.s ⊢ < = ( lt ‘ 𝐾 )
7 ishlati.j ⊢ ∨ = ( join ‘ 𝐾 )
8 ishlati.z ⊢ 0 = ( 0. ‘ 𝐾 )
9 ishlati.u ⊢ 1 = ( 1. ‘ 𝐾 )
10 ishlati.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
11 ishlati.9 ⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ ( 𝑧 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑧 ∨ 𝑥 ) ) )
12 ishlati.10 ⊢ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) )
13 1 2 3 3pm3.2i ⊢ ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat )
14 11 12 pm3.2i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ ( 𝑧 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑧 ∨ 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )
15 4 5 6 7 8 9 10 ishlat2 ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ ( 𝑧 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑧 ∨ 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
16 13 14 15 mpbir2an ⊢ 𝐾 ∈ HL