This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )