This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 } ) )