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 B = Base K
hlhgt4.s < ˙ = < K
hlhgt4.z 0 ˙ = 0. K
hlhgt4.u 1 ˙ = 1. K
Assertion hlhgt4 K HL x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 hlhgt4.b B = Base K
2 hlhgt4.s < ˙ = < K
3 hlhgt4.z 0 ˙ = 0. K
4 hlhgt4.u 1 ˙ = 1. K
5 eqid K = K
6 eqid join K = join K
7 eqid Atoms K = Atoms K
8 1 5 2 6 3 4 7 ishlat2 K HL K OML K CLat K AtLat x Atoms K y Atoms K x y z Atoms K z x z y z K x join K y z B ¬ x K z x K z join K y y K z join K x x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
9 simprr K OML K CLat K AtLat x Atoms K y Atoms K x y z Atoms K z x z y z K x join K y z B ¬ x K z x K z join K y y K z join K x x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙ x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙
10 8 9 sylbi K HL x B y B z B 0 ˙ < ˙ x x < ˙ y y < ˙ z z < ˙ 1 ˙