Metamath Proof Explorer

Theorem dicfval

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 )
dicval.p 
|- P = ( ( oc ` K ) ` W )
dicval.t 
|- T = ( ( LTrn ` K ) ` W )
dicval.e 
|- E = ( ( TEndo ` K ) ` W )
dicval.i 
|- I = ( ( DIsoC ` K ) ` W )
Assertion dicfval 
|- ( ( K e. V /\ W e. H ) -> I = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )

Proof

Step Hyp Ref Expression
1 dicval.l 
 |-  .<_ = ( le ` K )
2 dicval.a 
 |-  A = ( Atoms ` K )
3 dicval.h 
 |-  H = ( LHyp ` K )
4 dicval.p 
 |-  P = ( ( oc ` K ) ` W )
5 dicval.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 dicval.e 
 |-  E = ( ( TEndo ` K ) ` W )
7 dicval.i 
 |-  I = ( ( DIsoC ` K ) ` W )
8 1 2 3 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 ) ) } ) ) )
9 8 fveq1d 
 |-  ( K e. V -> ( ( DIsoC ` 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 ) ) } ) ) ` W ) )
10 7 9 syl5eq 
 |-  ( K e. V -> I = ( ( 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 ) ) } ) ) ` W ) )
11 breq2 
 |-  ( w = W -> ( r .<_ w <-> r .<_ W ) )
12 11 notbid 
 |-  ( w = W -> ( -. r .<_ w <-> -. r .<_ W ) )
13 12 rabbidv 
 |-  ( w = W -> { r e. A | -. r .<_ w } = { r e. A | -. r .<_ W } )
14 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
15 14 5 eqtr4di 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = T )
16 fveq2 
 |-  ( w = W -> ( ( oc ` K ) ` w ) = ( ( oc ` K ) ` W ) )
17 16 4 eqtr4di 
 |-  ( w = W -> ( ( oc ` K ) ` w ) = P )
18 17 fveqeq2d 
 |-  ( w = W -> ( ( g ` ( ( oc ` K ) ` w ) ) = q <-> ( g ` P ) = q ) )
19 15 18 riotaeqbidv 
 |-  ( w = W -> ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) = ( iota_ g e. T ( g ` P ) = q ) )
20 19 fveq2d 
 |-  ( w = W -> ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) )
21 20 eqeq2d 
 |-  ( w = W -> ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) <-> f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) ) )
22 fveq2 
 |-  ( w = W -> ( ( TEndo ` K ) ` w ) = ( ( TEndo ` K ) ` W ) )
23 22 6 eqtr4di 
 |-  ( w = W -> ( ( TEndo ` K ) ` w ) = E )
24 23 eleq2d 
 |-  ( w = W -> ( s e. ( ( TEndo ` K ) ` w ) <-> s e. E ) )
25 21 24 anbi12d 
 |-  ( w = W -> ( ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` w ) ( g ` ( ( oc ` K ) ` w ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` w ) ) <-> ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) ) )
26 25 opabbidv 
 |-  ( w = W -> { <. 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. T ( g ` P ) = q ) ) /\ s e. E ) } )
27 13 26 mpteq12dv 
 |-  ( w = 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 ) ) } ) = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )
28 eqid 
 |-  ( 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 ) ) } ) ) = ( 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 2 fvexi 
 |-  A e. _V
30 29 mptrabex 
 |-  ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) e. _V
31 27 28 30 fvmpt 
 |-  ( W e. H -> ( ( 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 ) ) } ) ) ` W ) = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )
32 10 31 sylan9eq 
 |-  ( ( K e. V /\ W e. H ) -> I = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )