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