Metamath Proof Explorer

Theorem dicffval

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

Ref Expression
Hypotheses dicval.l 
|- .<_ = ( le ` K )
dicval.a 
|- A = ( Atoms ` K )
dicval.h 
|- H = ( LHyp ` K )
Assertion dicffval 
|- ( K e. V -> ( DIsoC ` K ) = ( w e. H |-> ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 dicval.l 
 |-  .<_ = ( le ` K )
2 dicval.a 
 |-  A = ( Atoms ` K )
3 dicval.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 -> ( Atoms ` k ) = ( Atoms ` K ) )
8 7 2 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
9 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
10 9 1 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
11 10 breqd 
 |-  ( k = K -> ( r ( le ` k ) w <-> r .<_ w ) )
12 11 notbid 
 |-  ( k = K -> ( -. r ( le ` k ) w <-> -. r .<_ w ) )
13 8 12 rabeqbidv 
 |-  ( k = K -> { r e. ( Atoms ` k ) | -. r ( le ` k ) w } = { r e. A | -. r .<_ w } )
14 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
15 14 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
16 fveq2 
 |-  ( k = K -> ( oc ` k ) = ( oc ` K ) )
17 16 fveq1d 
 |-  ( k = K -> ( ( oc ` k ) ` w ) = ( ( oc ` K ) ` w ) )
18 17 fveqeq2d 
 |-  ( k = K -> ( ( g ` ( ( oc ` k ) ` w ) ) = q <-> ( g ` ( ( oc ` K ) ` w ) ) = q ) )
19 15 18 riotaeqbidv 
 |-  ( k = K -> ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) = ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) )
20 19 fveq2d 
 |-  ( k = K -> ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) )
21 20 eqeq2d 
 |-  ( k = K -> ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) <-> f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) ) )
22 fveq2 
 |-  ( k = K -> ( TEndo ` k ) = ( TEndo ` K ) )
23 22 fveq1d 
 |-  ( k = K -> ( ( TEndo ` k ) ` w ) = ( ( TEndo ` K ) ` w ) )
24 23 eleq2d 
 |-  ( k = K -> ( s e. ( ( TEndo ` k ) ` w ) <-> s e. ( ( TEndo ` K ) ` w ) ) )
25 21 24 anbi12d 
 |-  ( k = K -> ( ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) <-> ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) ) )
26 25 opabbidv 
 |-  ( k = K -> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } )
27 13 26 mpteq12dv 
 |-  ( k = K -> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) = ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) )
28 6 27 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) = ( w e. H |-> ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) ) )
29 df-dic 
 |-  DIsoC = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( q e. { r e. ( Atoms ` k ) | -. r ( le ` k ) w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` k ) ` w ) ( g ` ( ( oc ` k ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` k ) ` w ) ) } ) ) )
30 28 29 3 mptfvmpt 
 |-  ( K e. _V -> ( DIsoC ` K ) = ( w e. H |-> ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) ) )
31 4 30 syl 
 |-  ( K e. V -> ( DIsoC ` K ) = ( w e. H |-> ( q e. { r e. A | -. r .<_ w } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) } ) ) )