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

Metamath Proof Explorer

Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unity. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 22-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses pmap1.u 
|- .1. = ( 1. ` K )
pmap1.a 
|- A = ( Atoms ` K )
pmap1.m 
|- M = ( pmap ` K )
Assertion pmap1N 
|- ( K e. OP -> ( M ` .1. ) = A )

Proof

Step Hyp Ref Expression
1 pmap1.u 
 |-  .1. = ( 1. ` K )
2 pmap1.a 
 |-  A = ( Atoms ` K )
3 pmap1.m 
 |-  M = ( pmap ` K )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 4 1 op1cl 
 |-  ( K e. OP -> .1. e. ( Base ` K ) )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 4 6 2 3 pmapval 
 |-  ( ( K e. OP /\ .1. e. ( Base ` K ) ) -> ( M ` .1. ) = { p e. A | p ( le ` K ) .1. } )
8 5 7 mpdan 
 |-  ( K e. OP -> ( M ` .1. ) = { p e. A | p ( le ` K ) .1. } )
9 4 2 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
10 4 6 1 ople1 
 |-  ( ( K e. OP /\ p e. ( Base ` K ) ) -> p ( le ` K ) .1. )
11 9 10 sylan2 
 |-  ( ( K e. OP /\ p e. A ) -> p ( le ` K ) .1. )
12 11 ralrimiva 
 |-  ( K e. OP -> A. p e. A p ( le ` K ) .1. )
13 rabid2 
 |-  ( A = { p e. A | p ( le ` K ) .1. } <-> A. p e. A p ( le ` K ) .1. )
14 12 13 sylibr 
 |-  ( K e. OP -> A = { p e. A | p ( le ` K ) .1. } )
15 8 14 eqtr4d 
 |-  ( K e. OP -> ( M ` .1. ) = A )