Metamath Proof Explorer

Theorem ldilfset

Description: The mapping from fiducial co-atom w to its set of lattice dilations. (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ldilset.b 
|- B = ( Base ` K )
ldilset.l 
|- .<_ = ( le ` K )
ldilset.h 
|- H = ( LHyp ` K )
ldilset.i 
|- I = ( LAut ` K )
Assertion ldilfset 
|- ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )

Proof

Step Hyp Ref Expression
1 ldilset.b 
 |-  B = ( Base ` K )
2 ldilset.l 
 |-  .<_ = ( le ` K )
3 ldilset.h 
 |-  H = ( LHyp ` K )
4 ldilset.i 
 |-  I = ( LAut ` K )
5 elex 
 |-  ( K e. C -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
7 6 3 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
8 fveq2 
 |-  ( k = K -> ( LAut ` k ) = ( LAut ` K ) )
9 8 4 eqtr4di 
 |-  ( k = K -> ( LAut ` k ) = I )
10 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
11 10 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
12 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
13 12 2 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
14 13 breqd 
 |-  ( k = K -> ( x ( le ` k ) w <-> x .<_ w ) )
15 14 imbi1d 
 |-  ( k = K -> ( ( x ( le ` k ) w -> ( f ` x ) = x ) <-> ( x .<_ w -> ( f ` x ) = x ) ) )
16 11 15 raleqbidv 
 |-  ( k = K -> ( A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) <-> A. x e. B ( x .<_ w -> ( f ` x ) = x ) ) )
17 9 16 rabeqbidv 
 |-  ( k = K -> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } = { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } )
18 7 17 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )
19 df-ldil 
 |-  LDil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )
20 18 19 3 mptfvmpt 
 |-  ( K e. _V -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )
21 5 20 syl 
 |-  ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )