Theorem pmapat

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

	Ref	Expression
Hypotheses	pmapat.a	|- A = ( Atoms ` K )
	pmapat.m	|- M = ( pmap ` K )
Assertion	pmapat	|- ( ( K e. HL /\ P e. A ) -> ( M ` P ) = { P } )

Proof

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 e. A -> P e. ( Base ` K ) )
5		eqid	|- ( le ` K ) = ( le ` K )
6	3 5 1 2	pmapval	|- ( ( K e. HL /\ P e. ( Base ` K ) ) -> ( M ` P ) = { q e. A | q ( le ` K ) P } )
7	4 6	sylan2	|- ( ( K e. HL /\ P e. A ) -> ( M ` P ) = { q e. A | q ( le ` K ) P } )
8		hlatl	|- ( K e. HL -> K e. AtLat )
9	8	ad2antrr	|- ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> K e. AtLat )
10		simpr	|- ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> q e. A )
11		simplr	|- ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> P e. A )
12	5 1	atcmp	|- ( ( K e. AtLat /\ q e. A /\ P e. A ) -> ( q ( le ` K ) P <-> q = P ) )
13	9 10 11 12	syl3anc	|- ( ( ( K e. HL /\ P e. A ) /\ q e. A ) -> ( q ( le ` K ) P <-> q = P ) )
14	13	rabbidva	|- ( ( K e. HL /\ P e. A ) -> { q e. A | q ( le ` K ) P } = { q e. A | q = P } )
15		rabsn	|- ( P e. A -> { q e. A | q = P } = { P } )
16	15	adantl	|- ( ( K e. HL /\ P e. A ) -> { q e. A | q = P } = { P } )
17	7 14 16	3eqtrd	|- ( ( K e. HL /\ P e. A ) -> ( M ` P ) = { P } )