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. ) = (/) )