Theorem pmap1N

Description: Value of the projective map of a Hilbert lattice at lattice unit. 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 )