pmapat

Description: The projective map of an atom. (Contributed by NM, 25-Jan-2012)

Step	Hyp	Ref	Expression
1		pmapat.a	$⊢ A = Atoms (K)$
2		pmapat.m	$⊢ M = pmap (K)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4	3 1	atbase	$⊢ P \in A \to P \in {Base}_{K}$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	3 5 1 2	pmapval	$⊢ (K \in HL \land P \in {Base}_{K}) \to M (P) = \{q \in A \| q \leq_{K} P\}$
7	4 6	sylan2	$⊢ (K \in HL \land P \in A) \to M (P) = \{q \in A \| q \leq_{K} P\}$
8		hlatl	$⊢ K \in HL \to K \in AtLat$
9	8	ad2antrr	$⊢ ((K \in HL \land P \in A) \land q \in A) \to K \in AtLat$
10		simpr	$⊢ ((K \in HL \land P \in A) \land q \in A) \to q \in A$
11		simplr	$⊢ ((K \in HL \land P \in A) \land q \in A) \to P \in A$
12	5 1	atcmp	$⊢ (K \in AtLat \land q \in A \land P \in A) \to (q \leq_{K} P \leftrightarrow q = P)$
13	9 10 11 12	syl3anc	$⊢ ((K \in HL \land P \in A) \land q \in A) \to (q \leq_{K} P \leftrightarrow q = P)$
14	13	rabbidva	$⊢ (K \in HL \land P \in A) \to \{q \in A \| q \leq_{K} P\} = \{q \in A \| q = P\}$
15		rabsn	$⊢ P \in A \to \{q \in A \| q = P\} = \{P\}$
16	15	adantl	$⊢ (K \in HL \land P \in A) \to \{q \in A \| q = P\} = \{P\}$
17	7 14 16	3eqtrd	$⊢ (K \in HL \land P \in A) \to M (P) = \{P\}$

Metamath Proof Explorer