Theorem isatl

Description: The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011) (Revised by NM, 14-Sep-2018)

	Ref	Expression
Hypotheses	isatlat.b	$$⊢B={\mathrm{Base}}_K$$
	isatlat.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	isatlat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isatlat.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	isatlat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	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 \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isatlat.b	$$⊢B={\mathrm{Base}}_K$$
2		isatlat.g	$$⊢G=\mathrm{glb}\left(K\right)$$
3		isatlat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
4		isatlat.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
5		isatlat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
7	6 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
8		fveq2	$$⊢k=K\to \mathrm{glb}\left(k\right)=\mathrm{glb}\left(K\right)$$
9	8 2	eqtr4di	$$⊢k=K\to \mathrm{glb}\left(k\right)=G$$
10	9	dmeqd	$$⊢k=K\to \mathrm{dom}\mathrm{glb}\left(k\right)=\mathrm{dom}G$$
11	7 10	eleq12d	$$⊢k=K\to \left({\mathrm{Base}}_k\in \mathrm{dom}\mathrm{glb}\left(k\right)\leftrightarrow B\in \mathrm{dom}G\right)$$
12		fveq2	$$⊢k=K\to \mathrm{0.}\left(k\right)=\mathrm{0.}\left(K\right)$$
13	12 4	eqtr4di	$$⊢k=K\to \mathrm{0.}\left(k\right)=\underset{\dot{}}{0}$$
14	13	neeq2d	$$⊢k=K\to \left(x\ne \mathrm{0.}\left(k\right)\leftrightarrow x\ne \underset{\dot{}}{0}\right)$$
15		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
16	15 5	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
17		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
18	17 3	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
19	18	breqd	$$⊢k=K\to \left(y{\le }_{k}x\leftrightarrow y\underset{\dot{}}{\le }x\right)$$
20	16 19	rexeqbidv	$$⊢k=K\to \left(\exists y\in \mathrm{Atoms}\left(k\right)y{\le }_{k}x\leftrightarrow \exists y\in Ay\underset{\dot{}}{\le }x\right)$$
21	14 20	imbi12d	$$⊢k=K\to \left(\left(x\ne \mathrm{0.}\left(k\right)\to \exists y\in \mathrm{Atoms}\left(k\right)y{\le }_{k}x\right)\leftrightarrow \left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)$$
22	7 21	raleqbidv	$$⊢k=K\to \left(\forall x\in {\mathrm{Base}}_k\left(x\ne \mathrm{0.}\left(k\right)\to \exists y\in \mathrm{Atoms}\left(k\right)y{\le }_{k}x\right)\leftrightarrow \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)$$
23	11 22	anbi12d	$$⊢k=K\to \left(\left({\mathrm{Base}}_k\in \mathrm{dom}\mathrm{glb}\left(k\right)\wedge \forall x\in {\mathrm{Base}}_k\left(x\ne \mathrm{0.}\left(k\right)\to \exists y\in \mathrm{Atoms}\left(k\right)y{\le }_{k}x\right)\right)\leftrightarrow \left(B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)\right)$$
24		df-atl	$$⊢\mathrm{AtLat}=\left\{k\in \mathrm{Lat}|\left({\mathrm{Base}}_k\in \mathrm{dom}\mathrm{glb}\left(k\right)\wedge \forall x\in {\mathrm{Base}}_k\left(x\ne \mathrm{0.}\left(k\right)\to \exists y\in \mathrm{Atoms}\left(k\right)y{\le }_{k}x\right)\right)\right\}$$
25	23 24	elrab2	$$⊢K\in \mathrm{AtLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge \left(B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)\right)$$
26		3anass	$$⊢\left(K\in \mathrm{Lat}\wedge B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(K\in \mathrm{Lat}\wedge \left(B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)\right)$$
27	25 26	bitr4i	$$⊢K\in \mathrm{AtLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge B\in \mathrm{dom}G\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)$$