pmapglbx

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb , where we read S as S ( i ) . Theorem 15.5.2 of MaedaMaeda p. 62. (Contributed by NM, 5-Dec-2011)

	Ref	Expression
Hypotheses	pmapglb.b	$⊢ B = {Base}_{K}$
	pmapglb.g	$⊢ G = glb (K)$
	pmapglb.m	$⊢ M = pmap (K)$
Assertion	pmapglbx	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to M (G (\{y \| \exists i \in I y = S\})) = ⋂_{i \in I} M (S)$

Proof

Step	Hyp	Ref	Expression
1		pmapglb.b	$⊢ B = {Base}_{K}$
2		pmapglb.g	$⊢ G = glb (K)$
3		pmapglb.m	$⊢ M = pmap (K)$
4		hlclat	$⊢ K \in HL \to K \in CLat$
5	4	ad2antrr	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to K \in CLat$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	1 6	atbase	$⊢ p \in Atoms (K) \to p \in B$
8	7	adantl	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to p \in B$
9		r19.29	$⊢ (\forall i \in I S \in B \land \exists i \in I y = S) \to \exists i \in I (S \in B \land y = S)$
10		eleq1a	$⊢ S \in B \to (y = S \to y \in B)$
11	10	imp	$⊢ (S \in B \land y = S) \to y \in B$
12	11	rexlimivw	$⊢ \exists i \in I (S \in B \land y = S) \to y \in B$
13	9 12	syl	$⊢ (\forall i \in I S \in B \land \exists i \in I y = S) \to y \in B$
14	13	ex	$⊢ \forall i \in I S \in B \to (\exists i \in I y = S \to y \in B)$
15	14	ad2antlr	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to (\exists i \in I y = S \to y \in B)$
16	15	abssdv	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to \{y \| \exists i \in I y = S\} \subseteq B$
17		eqid	$⊢ \leq_{K} = \leq_{K}$
18	1 17 2	clatleglb	$⊢ (K \in CLat \land p \in B \land \{y \| \exists i \in I y = S\} \subseteq B) \to (p \leq_{K} G (\{y \| \exists i \in I y = S\}) \leftrightarrow \forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z)$
19	5 8 16 18	syl3anc	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to (p \leq_{K} G (\{y \| \exists i \in I y = S\}) \leftrightarrow \forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z)$
20		vex	$⊢ z \in V$
21		eqeq1	$⊢ y = z \to (y = S \leftrightarrow z = S)$
22	21	rexbidv	$⊢ y = z \to (\exists i \in I y = S \leftrightarrow \exists i \in I z = S)$
23	20 22	elab	$⊢ z \in \{y \| \exists i \in I y = S\} \leftrightarrow \exists i \in I z = S$
24	23	imbi1i	$⊢ (z \in \{y \| \exists i \in I y = S\} \to p \leq_{K} z) \leftrightarrow (\exists i \in I z = S \to p \leq_{K} z)$
25		r19.23v	$⊢ \forall i \in I (z = S \to p \leq_{K} z) \leftrightarrow (\exists i \in I z = S \to p \leq_{K} z)$
26	24 25	bitr4i	$⊢ (z \in \{y \| \exists i \in I y = S\} \to p \leq_{K} z) \leftrightarrow \forall i \in I (z = S \to p \leq_{K} z)$
27	26	albii	$⊢ \forall z (z \in \{y \| \exists i \in I y = S\} \to p \leq_{K} z) \leftrightarrow \forall z \forall i \in I (z = S \to p \leq_{K} z)$
28		df-ral	$⊢ \forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z \leftrightarrow \forall z (z \in \{y \| \exists i \in I y = S\} \to p \leq_{K} z)$
29		ralcom4	$⊢ \forall i \in I \forall z (z = S \to p \leq_{K} z) \leftrightarrow \forall z \forall i \in I (z = S \to p \leq_{K} z)$
30	27 28 29	3bitr4i	$⊢ \forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z \leftrightarrow \forall i \in I \forall z (z = S \to p \leq_{K} z)$
31		nfv	$⊢ Ⅎ z p \leq_{K} S$
32		breq2	$⊢ z = S \to (p \leq_{K} z \leftrightarrow p \leq_{K} S)$
33	31 32	ceqsalg	$⊢ S \in B \to (\forall z (z = S \to p \leq_{K} z) \leftrightarrow p \leq_{K} S)$
34	33	ralimi	$⊢ \forall i \in I S \in B \to \forall i \in I (\forall z (z = S \to p \leq_{K} z) \leftrightarrow p \leq_{K} S)$
35		ralbi	$⊢ \forall i \in I (\forall z (z = S \to p \leq_{K} z) \leftrightarrow p \leq_{K} S) \to (\forall i \in I \forall z (z = S \to p \leq_{K} z) \leftrightarrow \forall i \in I p \leq_{K} S)$
36	34 35	syl	$⊢ \forall i \in I S \in B \to (\forall i \in I \forall z (z = S \to p \leq_{K} z) \leftrightarrow \forall i \in I p \leq_{K} S)$
37	30 36	syl5bb	$⊢ \forall i \in I S \in B \to (\forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z \leftrightarrow \forall i \in I p \leq_{K} S)$
38	37	ad2antlr	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to (\forall z \in \{y \| \exists i \in I y = S\} p \leq_{K} z \leftrightarrow \forall i \in I p \leq_{K} S)$
39	19 38	bitrd	$⊢ ((K \in HL \land \forall i \in I S \in B) \land p \in Atoms (K)) \to (p \leq_{K} G (\{y \| \exists i \in I y = S\}) \leftrightarrow \forall i \in I p \leq_{K} S)$
40	39	rabbidva	$⊢ (K \in HL \land \forall i \in I S \in B) \to \{p \in Atoms (K) \| p \leq_{K} G (\{y \| \exists i \in I y = S\})\} = \{p \in Atoms (K) \| \forall i \in I p \leq_{K} S\}$
41	40	3adant3	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to \{p \in Atoms (K) \| p \leq_{K} G (\{y \| \exists i \in I y = S\})\} = \{p \in Atoms (K) \| \forall i \in I p \leq_{K} S\}$
42		simp1	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to K \in HL$
43	14	abssdv	$⊢ \forall i \in I S \in B \to \{y \| \exists i \in I y = S\} \subseteq B$
44	1 2	clatglbcl	$⊢ (K \in CLat \land \{y \| \exists i \in I y = S\} \subseteq B) \to G (\{y \| \exists i \in I y = S\}) \in B$
45	4 43 44	syl2an	$⊢ (K \in HL \land \forall i \in I S \in B) \to G (\{y \| \exists i \in I y = S\}) \in B$
46	45	3adant3	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to G (\{y \| \exists i \in I y = S\}) \in B$
47	1 17 6 3	pmapval	$⊢ (K \in HL \land G (\{y \| \exists i \in I y = S\}) \in B) \to M (G (\{y \| \exists i \in I y = S\})) = \{p \in Atoms (K) \| p \leq_{K} G (\{y \| \exists i \in I y = S\})\}$
48	42 46 47	syl2anc	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to M (G (\{y \| \exists i \in I y = S\})) = \{p \in Atoms (K) \| p \leq_{K} G (\{y \| \exists i \in I y = S\})\}$
49		iinrab	$⊢ I \neq \emptyset \to ⋂_{i \in I} \{p \in Atoms (K) \| p \leq_{K} S\} = \{p \in Atoms (K) \| \forall i \in I p \leq_{K} S\}$
50	49	3ad2ant3	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to ⋂_{i \in I} \{p \in Atoms (K) \| p \leq_{K} S\} = \{p \in Atoms (K) \| \forall i \in I p \leq_{K} S\}$
51	41 48 50	3eqtr4d	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to M (G (\{y \| \exists i \in I y = S\})) = ⋂_{i \in I} \{p \in Atoms (K) \| p \leq_{K} S\}$
52		nfv	$⊢ Ⅎ i K \in HL$
53		nfra1	$⊢ Ⅎ i \forall i \in I S \in B$
54		nfv	$⊢ Ⅎ i I \neq \emptyset$
55	52 53 54	nf3an	$⊢ Ⅎ i (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset)$
56		simpl1	$⊢ ((K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \land i \in I) \to K \in HL$
57		rspa	$⊢ (\forall i \in I S \in B \land i \in I) \to S \in B$
58	57	3ad2antl2	$⊢ ((K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \land i \in I) \to S \in B$
59	1 17 6 3	pmapval	$⊢ (K \in HL \land S \in B) \to M (S) = \{p \in Atoms (K) \| p \leq_{K} S\}$
60	56 58 59	syl2anc	$⊢ ((K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \land i \in I) \to M (S) = \{p \in Atoms (K) \| p \leq_{K} S\}$
61	55 60	iineq2d	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to ⋂_{i \in I} M (S) = ⋂_{i \in I} \{p \in Atoms (K) \| p \leq_{K} S\}$
62	51 61	eqtr4d	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to M (G (\{y \| \exists i \in I y = S\})) = ⋂_{i \in I} M (S)$

Metamath Proof Explorer

Theorem pmapglbx

Proof