pmapglb2xN

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N , where we read S as S ( i ) . Extension of Theorem 15.5.2 of MaedaMaeda p. 62 that allows I = (/) . (Contributed by NM, 21-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapglb2.b	$⊢ B = {Base}_{K}$
	pmapglb2.g	$⊢ G = glb (K)$
	pmapglb2.a	$⊢ A = Atoms (K)$
	pmapglb2.m	$⊢ M = pmap (K)$
Assertion	pmapglb2xN	$⊢ (K \in HL \land \forall i \in I S \in B) \to M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S)$

Proof

Step	Hyp	Ref	Expression
1		pmapglb2.b	$⊢ B = {Base}_{K}$
2		pmapglb2.g	$⊢ G = glb (K)$
3		pmapglb2.a	$⊢ A = Atoms (K)$
4		pmapglb2.m	$⊢ M = pmap (K)$
5		hlop	$⊢ K \in HL \to K \in OP$
6		eqid	$⊢ 1. (K) = 1. (K)$
7	2 6	glb0N	$⊢ K \in OP \to G (\emptyset) = 1. (K)$
8	7	fveq2d	$⊢ K \in OP \to M (G (\emptyset)) = M (1. (K))$
9	6 3 4	pmap1N	$⊢ K \in OP \to M (1. (K)) = A$
10	8 9	eqtrd	$⊢ K \in OP \to M (G (\emptyset)) = A$
11	5 10	syl	$⊢ K \in HL \to M (G (\emptyset)) = A$
12		rexeq	$⊢ I = \emptyset \to (\exists i \in I y = S \leftrightarrow \exists i \in \emptyset y = S)$
13	12	abbidv	$⊢ I = \emptyset \to \{y \| \exists i \in I y = S\} = \{y \| \exists i \in \emptyset y = S\}$
14		rex0	$⊢ \neg \exists i \in \emptyset y = S$
15	14	abf	$⊢ \{y \| \exists i \in \emptyset y = S\} = \emptyset$
16	13 15	eqtrdi	$⊢ I = \emptyset \to \{y \| \exists i \in I y = S\} = \emptyset$
17	16	fveq2d	$⊢ I = \emptyset \to G (\{y \| \exists i \in I y = S\}) = G (\emptyset)$
18	17	fveq2d	$⊢ I = \emptyset \to M (G (\{y \| \exists i \in I y = S\})) = M (G (\emptyset))$
19		riin0	$⊢ I = \emptyset \to A \cap ⋂_{i \in I} M (S) = A$
20	18 19	eqeq12d	$⊢ I = \emptyset \to (M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S) \leftrightarrow M (G (\emptyset)) = A)$
21	11 20	syl5ibrcom	$⊢ K \in HL \to (I = \emptyset \to M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S))$
22	21	adantr	$⊢ (K \in HL \land \forall i \in I S \in B) \to (I = \emptyset \to M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S))$
23	1 2 4	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)$
24		nfv	$⊢ Ⅎ i K \in HL$
25		nfra1	$⊢ Ⅎ i \forall i \in I S \in B$
26	24 25	nfan	$⊢ Ⅎ i (K \in HL \land \forall i \in I S \in B)$
27		simpr	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to i \in I$
28		simpll	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to K \in HL$
29		rspa	$⊢ (\forall i \in I S \in B \land i \in I) \to S \in B$
30	29	adantll	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to S \in B$
31	1 3 4	pmapssat	$⊢ (K \in HL \land S \in B) \to M (S) \subseteq A$
32	28 30 31	syl2anc	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to M (S) \subseteq A$
33	27 32	jca	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to (i \in I \land M (S) \subseteq A)$
34	33	ex	$⊢ (K \in HL \land \forall i \in I S \in B) \to (i \in I \to (i \in I \land M (S) \subseteq A))$
35	26 34	eximd	$⊢ (K \in HL \land \forall i \in I S \in B) \to (\exists i i \in I \to \exists i (i \in I \land M (S) \subseteq A))$
36		n0	$⊢ I \neq \emptyset \leftrightarrow \exists i i \in I$
37		df-rex	$⊢ \exists i \in I M (S) \subseteq A \leftrightarrow \exists i (i \in I \land M (S) \subseteq A)$
38	35 36 37	3imtr4g	$⊢ (K \in HL \land \forall i \in I S \in B) \to (I \neq \emptyset \to \exists i \in I M (S) \subseteq A)$
39	38	3impia	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to \exists i \in I M (S) \subseteq A$
40		iinss	$⊢ \exists i \in I M (S) \subseteq A \to ⋂_{i \in I} M (S) \subseteq A$
41	39 40	syl	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to ⋂_{i \in I} M (S) \subseteq A$
42		sseqin2	$⊢ ⋂_{i \in I} M (S) \subseteq A \leftrightarrow A \cap ⋂_{i \in I} M (S) = ⋂_{i \in I} M (S)$
43	41 42	sylib	$⊢ (K \in HL \land \forall i \in I S \in B \land I \neq \emptyset) \to A \cap ⋂_{i \in I} M (S) = ⋂_{i \in I} M (S)$
44	23 43	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\})) = A \cap ⋂_{i \in I} M (S)$
45	44	3expia	$⊢ (K \in HL \land \forall i \in I S \in B) \to (I \neq \emptyset \to M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S))$
46	22 45	pm2.61dne	$⊢ (K \in HL \land \forall i \in I S \in B) \to M (G (\{y \| \exists i \in I y = S\})) = A \cap ⋂_{i \in I} M (S)$

Metamath Proof Explorer

Theorem pmapglb2xN

Proof