pmapmeet

	Ref	Expression
Hypotheses	pmapmeet.b	$⊢ B = {Base}_{K}$
	pmapmeet.m	$⊢ \underset{˙}{\land} = meet (K)$
	pmapmeet.a	$⊢ A = Atoms (K)$
	pmapmeet.p	$⊢ P = pmap (K)$
Assertion	pmapmeet	$⊢ (K \in HL \land X \in B \land Y \in B) \to P (X \underset{˙}{\land} Y) = P (X) \cap P (Y)$

Proof

Step	Hyp	Ref	Expression
1		pmapmeet.b	$⊢ B = {Base}_{K}$
2		pmapmeet.m	$⊢ \underset{˙}{\land} = meet (K)$
3		pmapmeet.a	$⊢ A = Atoms (K)$
4		pmapmeet.p	$⊢ P = pmap (K)$
5		eqid	$⊢ glb (K) = glb (K)$
6		simp1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in HL$
7		simp2	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \in B$
8		simp3	$⊢ (K \in HL \land X \in B \land Y \in B) \to Y \in B$
9	5 2 6 7 8	meetval	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
10	9	fveq2d	$⊢ (K \in HL \land X \in B \land Y \in B) \to P (X \underset{˙}{\land} Y) = P (glb (K) (\{X, Y\}))$
11		prssi	$⊢ (X \in B \land Y \in B) \to \{X, Y\} \subseteq B$
12	11	3adant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to \{X, Y\} \subseteq B$
13		prnzg	$⊢ X \in B \to \{X, Y\} \neq \emptyset$
14	13	3ad2ant2	$⊢ (K \in HL \land X \in B \land Y \in B) \to \{X, Y\} \neq \emptyset$
15	1 5 4	pmapglb	$⊢ (K \in HL \land \{X, Y\} \subseteq B \land \{X, Y\} \neq \emptyset) \to P (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} P (x)$
16	6 12 14 15	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to P (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} P (x)$
17		fveq2	$⊢ x = X \to P (x) = P (X)$
18		fveq2	$⊢ x = Y \to P (x) = P (Y)$
19	17 18	iinxprg	$⊢ (X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} P (x) = P (X) \cap P (Y)$
20	19	3adant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} P (x) = P (X) \cap P (Y)$
21	10 16 20	3eqtrd	$⊢ (K \in HL \land X \in B \land Y \in B) \to P (X \underset{˙}{\land} Y) = P (X) \cap P (Y)$

Metamath Proof Explorer

Theorem pmapmeet

Proof