Theorem pmapfval

Description: The projective map of a Hilbert lattice. (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	pmapfval	|- ( K e. C -> M = ( x e. B |-> { 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		elex	|- ( K e. C -> K e. _V )
6		fveq2	|- ( k = K -> ( Base ` k ) = ( Base ` K ) )
7	6 1	eqtr4di	|- ( k = K -> ( Base ` k ) = B )
8		fveq2	|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
9	8 3	eqtr4di	|- ( k = K -> ( Atoms ` k ) = A )
10		fveq2	|- ( k = K -> ( le ` k ) = ( le ` K ) )
11	10 2	eqtr4di	|- ( k = K -> ( le ` k ) = .<_ )
12	11	breqd	|- ( k = K -> ( a ( le ` k ) x <-> a .<_ x ) )
13	9 12	rabeqbidv	|- ( k = K -> { a e. ( Atoms ` k ) | a ( le ` k ) x } = { a e. A | a .<_ x } )
14	7 13	mpteq12dv	|- ( k = K -> ( x e. ( Base ` k ) |-> { a e. ( Atoms ` k ) | a ( le ` k ) x } ) = ( x e. B |-> { a e. A | a .<_ x } ) )
15		df-pmap	|- pmap = ( k e. _V |-> ( x e. ( Base ` k ) |-> { a e. ( Atoms ` k ) | a ( le ` k ) x } ) )
16	14 15 1	mptfvmpt	|- ( K e. _V -> ( pmap ` K ) = ( x e. B |-> { a e. A | a .<_ x } ) )
17	4 16	syl5eq	|- ( K e. _V -> M = ( x e. B |-> { a e. A | a .<_ x } ) )
18	5 17	syl	|- ( K e. C -> M = ( x e. B |-> { a e. A | a .<_ x } ) )