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 ) ) ) )