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

Metamath Proof Explorer

Theorem pmap0

Description: Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of MaedaMaeda p. 62. (Contributed by NM, 17-Oct-2011)

Ref Expression
Hypotheses pmap0.z 
|- .0. = ( 0. ` K )
pmap0.m 
|- M = ( pmap ` K )
Assertion pmap0 
|- ( K e. AtLat -> ( M ` .0. ) = (/) )

Proof

Step Hyp Ref Expression
1 pmap0.z 
 |-  .0. = ( 0. ` K )
2 pmap0.m 
 |-  M = ( pmap ` K )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 3 1 atl0cl 
 |-  ( K e. AtLat -> .0. e. ( Base ` K ) )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 3 5 6 2 pmapval 
 |-  ( ( K e. AtLat /\ .0. e. ( Base ` K ) ) -> ( M ` .0. ) = { a e. ( Atoms ` K ) | a ( le ` K ) .0. } )
8 4 7 mpdan 
 |-  ( K e. AtLat -> ( M ` .0. ) = { a e. ( Atoms ` K ) | a ( le ` K ) .0. } )
9 5 1 6 atnle0 
 |-  ( ( K e. AtLat /\ a e. ( Atoms ` K ) ) -> -. a ( le ` K ) .0. )
10 9 nrexdv 
 |-  ( K e. AtLat -> -. E. a e. ( Atoms ` K ) a ( le ` K ) .0. )
11 rabn0 
 |-  ( { a e. ( Atoms ` K ) | a ( le ` K ) .0. } =/= (/) <-> E. a e. ( Atoms ` K ) a ( le ` K ) .0. )
12 10 11 sylnibr 
 |-  ( K e. AtLat -> -. { a e. ( Atoms ` K ) | a ( le ` K ) .0. } =/= (/) )
13 nne 
 |-  ( -. { a e. ( Atoms ` K ) | a ( le ` K ) .0. } =/= (/) <-> { a e. ( Atoms ` K ) | a ( le ` K ) .0. } = (/) )
14 12 13 sylib 
 |-  ( K e. AtLat -> { a e. ( Atoms ` K ) | a ( le ` K ) .0. } = (/) )
15 8 14 eqtrd 
 |-  ( K e. AtLat -> ( M ` .0. ) = (/) )