Metamath Proof Explorer

Theorem diaffval

Description: The partial isomorphism A for a lattice K . (Contributed by NM, 15-Oct-2013)

Ref Expression
Hypotheses diaval.b 
|- B = ( Base ` K )
diaval.l 
|- .<_ = ( le ` K )
diaval.h 
|- H = ( LHyp ` K )
Assertion diaffval 
|- ( K e. V -> ( DIsoA ` K ) = ( w e. H |-> ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) ) )

Proof

Step Hyp Ref Expression
1 diaval.b 
 |-  B = ( Base ` K )
2 diaval.l 
 |-  .<_ = ( le ` K )
3 diaval.h 
 |-  H = ( LHyp ` K )
4 elex 
 |-  ( K e. V -> K e. _V )
5 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
6 5 3 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
7 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
8 7 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
9 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
10 9 2 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
11 10 breqd 
 |-  ( k = K -> ( y ( le ` k ) w <-> y .<_ w ) )
12 8 11 rabeqbidv 
 |-  ( k = K -> { y e. ( Base ` k ) | y ( le ` k ) w } = { y e. B | y .<_ w } )
13 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
14 13 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
15 fveq2 
 |-  ( k = K -> ( trL ` k ) = ( trL ` K ) )
16 15 fveq1d 
 |-  ( k = K -> ( ( trL ` k ) ` w ) = ( ( trL ` K ) ` w ) )
17 16 fveq1d 
 |-  ( k = K -> ( ( ( trL ` k ) ` w ) ` f ) = ( ( ( trL ` K ) ` w ) ` f ) )
18 eqidd 
 |-  ( k = K -> x = x )
19 17 10 18 breq123d 
 |-  ( k = K -> ( ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x <-> ( ( ( trL ` K ) ` w ) ` f ) .<_ x ) )
20 14 19 rabeqbidv 
 |-  ( k = K -> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } = { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } )
21 12 20 mpteq12dv 
 |-  ( k = K -> ( x e. { y e. ( Base ` k ) | y ( le ` k ) w } |-> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } ) = ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) )
22 6 21 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. { y e. ( Base ` k ) | y ( le ` k ) w } |-> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } ) ) = ( w e. H |-> ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) ) )
23 df-disoa 
 |-  DIsoA = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. { y e. ( Base ` k ) | y ( le ` k ) w } |-> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } ) ) )
24 22 23 3 mptfvmpt 
 |-  ( K e. _V -> ( DIsoA ` K ) = ( w e. H |-> ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) ) )
25 4 24 syl 
 |-  ( K e. V -> ( DIsoA ` K ) = ( w e. H |-> ( x e. { y e. B | y .<_ w } |-> { f e. ( ( LTrn ` K ) ` w ) | ( ( ( trL ` K ) ` w ) ` f ) .<_ x } ) ) )