Theorem hlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	hlatle.b	$$⊢B={\mathrm{Base}}_K$$
	hlatle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlatle.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlatle	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlatle.b	$$⊢B={\mathrm{Base}}_K$$
2		hlatle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlatle.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		hlomcmat	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)$$
5	1 2 3	atlatle	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\right)$$
6	4 5	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \forall p\in A\left(p\underset{\dot{}}{\le }X\to p\underset{\dot{}}{\le }Y\right)\right)$$