Metamath Proof Explorer

Theorem pmapglb

Description: The projective map of the GLB of a set of lattice elements S . Variant of 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	pmapglb	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to M (G (S)) = ⋂_{x \in S} M (x)$

Proof

Step	Hyp	Ref	Expression
1		pmapglb.b	$⊢ B = {Base}_{K}$
2		pmapglb.g	$⊢ G = glb (K)$
3		pmapglb.m	$⊢ M = pmap (K)$
4		df-rex	$⊢ \exists x \in S y = x \leftrightarrow \exists x (x \in S \land y = x)$
5		equcom	$⊢ y = x \leftrightarrow x = y$
6	5	anbi1ci	$⊢ (x \in S \land y = x) \leftrightarrow (x = y \land x \in S)$
7	6	exbii	$⊢ \exists x (x \in S \land y = x) \leftrightarrow \exists x (x = y \land x \in S)$
8		eleq1w	$⊢ x = y \to (x \in S \leftrightarrow y \in S)$
9	8	equsexvw	$⊢ \exists x (x = y \land x \in S) \leftrightarrow y \in S$
10	4 7 9	3bitri	$⊢ \exists x \in S y = x \leftrightarrow y \in S$
11	10	abbii	$⊢ \{y \| \exists x \in S y = x\} = \{y \| y \in S\}$
12		abid2	$⊢ \{y \| y \in S\} = S$
13	11 12	eqtr2i	$⊢ S = \{y \| \exists x \in S y = x\}$
14	13	fveq2i	$⊢ G (S) = G (\{y \| \exists x \in S y = x\})$
15	14	fveq2i	$⊢ M (G (S)) = M (G (\{y \| \exists x \in S y = x\}))$
16		dfss3	$⊢ S \subseteq B \leftrightarrow \forall x \in S x \in B$
17	1 2 3	pmapglbx	$⊢ (K \in HL \land \forall x \in S x \in B \land S \neq \emptyset) \to M (G (\{y \| \exists x \in S y = x\})) = ⋂_{x \in S} M (x)$
18	16 17	syl3an2b	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to M (G (\{y \| \exists x \in S y = x\})) = ⋂_{x \in S} M (x)$
19	15 18	eqtrid	$⊢ (K \in HL \land S \subseteq B \land S \neq \emptyset) \to M (G (S)) = ⋂_{x \in S} M (x)$