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={\mathrm{Base}}_K$$
	hlhgt4.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	hlhgt4.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	hlhgt4.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	hlhgt4	$$⊢K\in \mathrm{HL}\to \exists x\in B\exists y\in B\exists z\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}y\right)\wedge \left(y\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlhgt4.b	$$⊢B={\mathrm{Base}}_K$$
2		hlhgt4.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		hlhgt4.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		hlhgt4.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
7		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
8	1 5 2 6 3 4 7	ishlat2	$$⊢K\in \mathrm{HL}\leftrightarrow \left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge \left(\forall x\in \mathrm{Atoms}\left(K\right)\forall y\in \mathrm{Atoms}\left(K\right)\left(\left(x\ne y\to \exists z\in \mathrm{Atoms}\left(K\right)\left(z\ne x\wedge z\ne y\wedge z{\le }_K\left(x\mathrm{join}\left(K\right)y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x{\le }_{K}z\wedge x{\le }_K\left(z\mathrm{join}\left(K\right)y\right)\right)\to y{\le }_K\left(z\mathrm{join}\left(K\right)x\right)\right)\right)\wedge \exists x\in B\exists y\in B\exists z\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}y\right)\wedge \left(y\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\right)\right)\right)$$
9		simprr	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge \left(\forall x\in \mathrm{Atoms}\left(K\right)\forall y\in \mathrm{Atoms}\left(K\right)\left(\left(x\ne y\to \exists z\in \mathrm{Atoms}\left(K\right)\left(z\ne x\wedge z\ne y\wedge z{\le }_K\left(x\mathrm{join}\left(K\right)y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x{\le }_{K}z\wedge x{\le }_K\left(z\mathrm{join}\left(K\right)y\right)\right)\to y{\le }_K\left(z\mathrm{join}\left(K\right)x\right)\right)\right)\wedge \exists x\in B\exists y\in B\exists z\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}y\right)\wedge \left(y\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\right)\right)\right)\to \exists x\in B\exists y\in B\exists z\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}y\right)\wedge \left(y\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\right)$$
10	8 9	sylbi	$$⊢K\in \mathrm{HL}\to \exists x\in B\exists y\in B\exists z\in B\left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}y\right)\wedge \left(y\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\right)$$