Metamath Proof Explorer

Theorem ishlat3N

Description: The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form E. z e. A ( x .\/ z ) = ( y .\/ z ) . The exchange property and atomicity are provided by K e. CvLat , and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses ishlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ishlat.l ⊢ ≤ = ( le ‘ 𝐾 )
ishlat.s ⊢ < = ( lt ‘ 𝐾 )
ishlat.j ⊢ ∨ = ( join ‘ 𝐾 )
ishlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
ishlat.u ⊢ 1 = ( 1. ‘ 𝐾 )
ishlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ishlat3N ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ishlat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 ishlat.s ⊢ < = ( lt ‘ 𝐾 )
4 ishlat.j ⊢ ∨ = ( join ‘ 𝐾 )
5 ishlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
6 ishlat.u ⊢ 1 = ( 1. ‘ 𝐾 )
7 ishlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 1 2 3 4 5 6 7 ishlat1 ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
9 simpll3 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
10 simplrl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
11 simplrr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
12 simpr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
13 7 2 4 cvlsupr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ↔ ( 𝑥 ≠ 𝑦 → ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
14 9 10 11 12 13 syl13anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ↔ ( 𝑥 ≠ 𝑦 → ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
15 14 rexbidva ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
16 ne0i ⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
17 16 ad2antrl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐴 ≠ ∅ )
18 r19.37zv ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
19 17 18 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
20 15 19 bitr2d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ) )
21 20 2ralbidva ⊢ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ) )
22 21 anbi1d ⊢ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
23 22 pm5.32i ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
24 8 23 bitri ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∨ 𝑧 ) = ( 𝑦 ∨ 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )