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=BaseK
hlhgt4.s <˙=<K
hlhgt4.z 0˙=0.K
hlhgt4.u 1˙=1.K
Assertion hlhgt4 KHLxByBzB0˙<˙xx<˙yy<˙zz<˙1˙

Proof

Step Hyp Ref Expression
1 hlhgt4.b B=BaseK
2 hlhgt4.s <˙=<K
3 hlhgt4.z 0˙=0.K
4 hlhgt4.u 1˙=1.K
5 eqid K=K
6 eqid joinK=joinK
7 eqid AtomsK=AtomsK
8 1 5 2 6 3 4 7 ishlat2 KHLKOMLKCLatKAtLatxAtomsKyAtomsKxyzAtomsKzxzyzKxjoinKyzB¬xKzxKzjoinKyyKzjoinKxxByBzB0˙<˙xx<˙yy<˙zz<˙1˙
9 simprr KOMLKCLatKAtLatxAtomsKyAtomsKxyzAtomsKzxzyzKxjoinKyzB¬xKzxKzjoinKyyKzjoinKxxByBzB0˙<˙xx<˙yy<˙zz<˙1˙xByBzB0˙<˙xx<˙yy<˙zz<˙1˙
10 8 9 sylbi KHLxByBzB0˙<˙xx<˙yy<˙zz<˙1˙