pmapglb2N

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. Allows S = (/) . (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	pmapglb2N	$⊢ (K \in HL \land S \subseteq B) \to M (G (S)) = A \cap ⋂_{x \in S} M (x)$

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		2fveq3	$⊢ S = \emptyset \to M (G (S)) = M (G (\emptyset))$
13		riin0	$⊢ S = \emptyset \to A \cap ⋂_{x \in S} M (x) = A$
14	12 13	eqeq12d	$⊢ S = \emptyset \to (M (G (S)) = A \cap ⋂_{x \in S} M (x) \leftrightarrow M (G (\emptyset)) = A)$
15	11 14	syl5ibrcom	$⊢ K \in HL \to (S = \emptyset \to M (G (S)) = A \cap ⋂_{x \in S} M (x))$
16	15	adantr	$⊢ (K \in HL \land S \subseteq B) \to (S = \emptyset \to M (G (S)) = A \cap ⋂_{x \in S} M (x))$
17	1 2 4	pmapglb	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to M (G (S)) = ⋂_{x \in S} M (x)$
18		simpr	$⊢ ((K \in HL \land S \subseteq B) \land x \in S) \to x \in S$
19		simpll	$⊢ ((K \in HL \land S \subseteq B) \land x \in S) \to K \in HL$
20		ssel2	$⊢ (S \subseteq B \land x \in S) \to x \in B$
21	20	adantll	$⊢ ((K \in HL \land S \subseteq B) \land x \in S) \to x \in B$
22	1 3 4	pmapssat	$⊢ (K \in HL \land x \in B) \to M (x) \subseteq A$
23	19 21 22	syl2anc	$⊢ ((K \in HL \land S \subseteq B) \land x \in S) \to M (x) \subseteq A$
24	18 23	jca	$⊢ ((K \in HL \land S \subseteq B) \land x \in S) \to (x \in S \land M (x) \subseteq A)$
25	24	ex	$⊢ (K \in HL \land S \subseteq B) \to (x \in S \to (x \in S \land M (x) \subseteq A))$
26	25	eximdv	$⊢ (K \in HL \land S \subseteq B) \to (\exists x x \in S \to \exists x (x \in S \land M (x) \subseteq A))$
27		n0	$⊢ S \neq \emptyset \leftrightarrow \exists x x \in S$
28		df-rex	$⊢ \exists x \in S M (x) \subseteq A \leftrightarrow \exists x (x \in S \land M (x) \subseteq A)$
29	26 27 28	3imtr4g	$⊢ (K \in HL \land S \subseteq B) \to (S \neq \emptyset \to \exists x \in S M (x) \subseteq A)$
30	29	3impia	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to \exists x \in S M (x) \subseteq A$
31		iinss	$⊢ \exists x \in S M (x) \subseteq A \to ⋂_{x \in S} M (x) \subseteq A$
32	30 31	syl	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to ⋂_{x \in S} M (x) \subseteq A$
33		sseqin2	$⊢ ⋂_{x \in S} M (x) \subseteq A \leftrightarrow A \cap ⋂_{x \in S} M (x) = ⋂_{x \in S} M (x)$
34	32 33	sylib	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to A \cap ⋂_{x \in S} M (x) = ⋂_{x \in S} M (x)$
35	17 34	eqtr4d	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to M (G (S)) = A \cap ⋂_{x \in S} M (x)$
36	35	3expia	$⊢ (K \in HL \land S \subseteq B) \to (S \neq \emptyset \to M (G (S)) = A \cap ⋂_{x \in S} M (x))$
37	16 36	pm2.61dne	$⊢ (K \in HL \land S \subseteq B) \to M (G (S)) = A \cap ⋂_{x \in S} M (x)$

Metamath Proof Explorer

Theorem pmapglb2N

Proof