Theorem atl0dm

Description: Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018)

	Ref	Expression
Hypotheses	atl01dm.b	$$⊢B={\mathrm{Base}}_K$$
	atl01dm.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	atl01dm.g	$$⊢G=\mathrm{glb}\left(K\right)$$
Assertion	atl0dm	$$⊢K\in \mathrm{AtLat}\to B\in \mathrm{dom}G$$

Proof

Step	Hyp	Ref	Expression
1		atl01dm.b	$$⊢B={\mathrm{Base}}_K$$
2		atl01dm.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		atl01dm.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
6		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
7	1 3 4 5 6	isatl	$$⊢K\in \mathrm{AtLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \mathrm{0.}\left(K\right)\to \exists y\in \mathrm{Atoms}\left(K\right)y{\le }_{K}x\right)\right)$$
8	7	simp2bi	$$⊢K\in \mathrm{AtLat}\to B\in \mathrm{dom}G$$