Theorem atl0cl

Description: An atomic lattice has a zero element. We can use this in place of op0cl for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atl0cl.b	$$⊢B={\mathrm{Base}}_K$$
	atl0cl.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in B$$

Proof

Step	Hyp	Ref	Expression
1		atl0cl.b	$$⊢B={\mathrm{Base}}_K$$
2		atl0cl.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
4	1 3 2	p0val	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}=\mathrm{glb}\left(K\right)\left(B\right)$$
5		id	$$⊢K\in \mathrm{AtLat}\to K\in \mathrm{AtLat}$$
6		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
7	1 6 3	atl0dm	$$⊢K\in \mathrm{AtLat}\to B\in \mathrm{dom}\mathrm{glb}\left(K\right)$$
8	1 3 5 7	glbcl	$$⊢K\in \mathrm{AtLat}\to \mathrm{glb}\left(K\right)\left(B\right)\in B$$
9	4 8	eqeltrd	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in B$$