Metamath Proof Explorer

Theorem dibffval

Description: The partial isomorphism B for a lattice K . (Contributed by NM, 8-Dec-2013)

Ref Expression
Hypotheses dibval.b 
|- B = ( Base ` K )
dibval.h 
|- H = ( LHyp ` K )
Assertion dibffval 
|- ( K e. V -> ( DIsoB ` K ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 dibval.b 
 |-  B = ( Base ` K )
2 dibval.h 
 |-  H = ( LHyp ` K )
3 elex 
 |-  ( K e. V -> K e. _V )
4 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
5 4 2 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
6 fveq2 
 |-  ( k = K -> ( DIsoA ` k ) = ( DIsoA ` K ) )
7 6 fveq1d 
 |-  ( k = K -> ( ( DIsoA ` k ) ` w ) = ( ( DIsoA ` K ) ` w ) )
8 7 dmeqd 
 |-  ( k = K -> dom ( ( DIsoA ` k ) ` w ) = dom ( ( DIsoA ` K ) ` w ) )
9 7 fveq1d 
 |-  ( k = K -> ( ( ( DIsoA ` k ) ` w ) ` x ) = ( ( ( DIsoA ` K ) ` w ) ` x ) )
10 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
11 10 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
12 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
13 12 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
14 13 reseq2d 
 |-  ( k = K -> ( _I |` ( Base ` k ) ) = ( _I |` B ) )
15 11 14 mpteq12dv 
 |-  ( k = K -> ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) = ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) )
16 15 sneqd 
 |-  ( k = K -> { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } = { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } )
17 9 16 xpeq12d 
 |-  ( k = K -> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) = ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) )
18 8 17 mpteq12dv 
 |-  ( k = K -> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) = ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) )
19 5 18 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )
20 df-dib 
 |-  DIsoB = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) ) )
21 19 20 2 mptfvmpt 
 |-  ( K e. _V -> ( DIsoB ` K ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )
22 3 21 syl 
 |-  ( K e. V -> ( DIsoB ` K ) = ( w e. H |-> ( x e. dom ( ( DIsoA ` K ) ` w ) |-> ( ( ( ( DIsoA ` K ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` K ) ` w ) |-> ( _I |` B ) ) } ) ) ) )