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 = {Base}_{K}$
	isatlat.g	$⊢ G = glb (K)$
	isatlat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	isatlat.z	$⊢ \underset{˙}{0} = 0. (K)$
	isatlat.a	$⊢ A = Atoms (K)$
Assertion	isatl	$⊢ K \in AtLat \leftrightarrow (K \in Lat \land B \in dom G \land \forall x \in B (x \neq \underset{˙}{0} \to \exists y \in A y \underset{˙}{\leq} x))$

Proof

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

Metamath Proof Explorer

Theorem isatl

Proof