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