Theorem pmapval

Description: Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 2-Oct-2011)

	Ref	Expression
Hypotheses	pmapfval.b	|- B = ( Base ` K )
	pmapfval.l	|- .<_ = ( le ` K )
	pmapfval.a	|- A = ( Atoms ` K )
	pmapfval.m	|- M = ( pmap ` K )
Assertion	pmapval	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) = { a e. A | a .<_ X } )

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	|- B = ( Base ` K )
2		pmapfval.l	|- .<_ = ( le ` K )
3		pmapfval.a	|- A = ( Atoms ` K )
4		pmapfval.m	|- M = ( pmap ` K )
5	1 2 3 4	pmapfval	|- ( K e. C -> M = ( x e. B |-> { a e. A | a .<_ x } ) )
6	5	fveq1d	|- ( K e. C -> ( M ` X ) = ( ( x e. B |-> { a e. A | a .<_ x } ) ` X ) )
7		breq2	|- ( x = X -> ( a .<_ x <-> a .<_ X ) )
8	7	rabbidv	|- ( x = X -> { a e. A | a .<_ x } = { a e. A | a .<_ X } )
9		eqid	|- ( x e. B |-> { a e. A | a .<_ x } ) = ( x e. B |-> { a e. A | a .<_ x } )
10	3	fvexi	|- A e. _V
11	10	rabex	|- { a e. A | a .<_ X } e. _V
12	8 9 11	fvmpt	|- ( X e. B -> ( ( x e. B |-> { a e. A | a .<_ x } ) ` X ) = { a e. A | a .<_ X } )
13	6 12	sylan9eq	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) = { a e. A | a .<_ X } )