This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isldil

Description: The predicate "is a lattice dilation". Similar to definition of dilation in Crawley p. 111. (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 isldil 
|- ( ( K e. C /\ W e. H ) -> ( F e. 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 5 ldilset 
 |-  ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
7 6 eleq2d 
 |-  ( ( K e. C /\ W e. H ) -> ( F e. D <-> F e. { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } ) )
8 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
9 8 eqeq1d 
 |-  ( f = F -> ( ( f ` x ) = x <-> ( F ` x ) = x ) )
10 9 imbi2d 
 |-  ( f = F -> ( ( x .<_ W -> ( f ` x ) = x ) <-> ( x .<_ W -> ( F ` x ) = x ) ) )
11 10 ralbidv 
 |-  ( f = F -> ( A. x e. B ( x .<_ W -> ( f ` x ) = x ) <-> A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) )
12 11 elrab 
 |-  ( F e. { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } <-> ( F e. I /\ A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) )
13 7 12 bitrdi 
 |-  ( ( K e. C /\ W e. H ) -> ( F e. D <-> ( F e. I /\ A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) ) )