Theorem ishlatiN

Description: Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ishlati.1	$$⊢K\in \mathrm{OML}$$
	ishlati.2	$$⊢K\in \mathrm{CLat}$$
	ishlati.3	$$⊢K\in \mathrm{AtLat}$$
	ishlati.b	$$⊢B={\mathrm{Base}}_K$$
	ishlati.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ishlati.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	ishlati.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	ishlati.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	ishlati.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
	ishlati.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ishlati.9	$$⊢\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)$$
	ishlati.10	$$⊢\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)$$
Assertion	ishlatiN	$$⊢K\in \mathrm{HL}$$

Proof

Step	Hyp	Ref	Expression
1		ishlati.1	$$⊢K\in \mathrm{OML}$$
2		ishlati.2	$$⊢K\in \mathrm{CLat}$$
3		ishlati.3	$$⊢K\in \mathrm{AtLat}$$
4		ishlati.b	$$⊢B={\mathrm{Base}}_K$$
5		ishlati.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6		ishlati.s	$$⊢\underset{\dot{}}{<}={<}_K$$
7		ishlati.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
8		ishlati.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
9		ishlati.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
10		ishlati.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
11		ishlati.9	$$⊢\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)$$
12		ishlati.10	$$⊢\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)$$
13	1 2 3	3pm3.2i	$$⊢\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)$$
14	11 12	pm3.2i	$$⊢\left(\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }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)$$
15	4 5 6 7 8 9 10	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 A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }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)$$
16	13 14 15	mpbir2an	$$⊢K\in \mathrm{HL}$$