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

Metamath Proof Explorer

Theorem hlhgt4

Description: A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011)

Ref Expression
Hypotheses hlhgt4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlhgt4.s ⊢ < = ( lt ‘ 𝐾 )
hlhgt4.z ⊢ 0 = ( 0. ‘ 𝐾 )
hlhgt4.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion hlhgt4 ( 𝐾 ∈ HL → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )

Proof

Step Hyp Ref Expression
1 hlhgt4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 hlhgt4.s ⊢ < = ( lt ‘ 𝐾 )
3 hlhgt4.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 hlhgt4.u ⊢ 1 = ( 1. ‘ 𝐾 )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 1 5 2 6 3 4 7 ishlat2 ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝐾 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ( le ‘ 𝐾 ) 𝑧 ∧ 𝑥 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
9 simprr ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝐾 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ( le ‘ 𝐾 ) 𝑧 ∧ 𝑥 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )
10 8 9 sylbi ⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )