Metamath Proof Explorer


Theorem ldilset

Description: The set of lattice dilations for a fiducial co-atom W . (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 )
ldilset.d
|- D = ( ( LDil ` K ) ` W )
Assertion ldilset
|- ( ( K e. C /\ W e. H ) -> D = { 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 ldilset.d
 |-  D = ( ( LDil ` K ) ` W )
6 1 2 3 4 ldilfset
 |-  ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )
7 6 fveq1d
 |-  ( K e. C -> ( ( LDil ` K ) ` W ) = ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) )
8 breq2
 |-  ( w = W -> ( x .<_ w <-> x .<_ W ) )
9 8 imbi1d
 |-  ( w = W -> ( ( x .<_ w -> ( f ` x ) = x ) <-> ( x .<_ W -> ( f ` x ) = x ) ) )
10 9 ralbidv
 |-  ( w = W -> ( A. x e. B ( x .<_ w -> ( f ` x ) = x ) <-> A. x e. B ( x .<_ W -> ( f ` x ) = x ) ) )
11 10 rabbidv
 |-  ( w = W -> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
12 eqid
 |-  ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } )
13 4 fvexi
 |-  I e. _V
14 13 rabex
 |-  { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } e. _V
15 11 12 14 fvmpt
 |-  ( W e. H -> ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
16 7 15 sylan9eq
 |-  ( ( K e. C /\ W e. H ) -> ( ( LDil ` K ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
17 5 16 syl5eq
 |-  ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )