Theorem idldil

Description: The identity function is a lattice dilation. (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	idldil.b	|- B = ( Base ` K )
	idldil.h	|- H = ( LHyp ` K )
	idldil.d	|- D = ( ( LDil ` K ) ` W )
Assertion	idldil	|- ( ( K e. A /\ W e. H ) -> ( _I |` B ) e. D )

Proof

Step	Hyp	Ref	Expression
1		idldil.b	|- B = ( Base ` K )
2		idldil.h	|- H = ( LHyp ` K )
3		idldil.d	|- D = ( ( LDil ` K ) ` W )
4		eqid	|- ( LAut ` K ) = ( LAut ` K )
5	1 4	idlaut	|- ( K e. A -> ( _I |` B ) e. ( LAut ` K ) )
6	5	adantr	|- ( ( K e. A /\ W e. H ) -> ( _I |` B ) e. ( LAut ` K ) )
7		fvresi	|- ( x e. B -> ( ( _I |` B ) ` x ) = x )
8	7	a1d	|- ( x e. B -> ( x ( le ` K ) W -> ( ( _I |` B ) ` x ) = x ) )
9	8	rgen	|- A. x e. B ( x ( le ` K ) W -> ( ( _I |` B ) ` x ) = x )
10	9	a1i	|- ( ( K e. A /\ W e. H ) -> A. x e. B ( x ( le ` K ) W -> ( ( _I |` B ) ` x ) = x ) )
11		eqid	|- ( le ` K ) = ( le ` K )
12	1 11 2 4 3	isldil	|- ( ( K e. A /\ W e. H ) -> ( ( _I |` B ) e. D <-> ( ( _I |` B ) e. ( LAut ` K ) /\ A. x e. B ( x ( le ` K ) W -> ( ( _I |` B ) ` x ) = x ) ) ) )
13	6 10 12	mpbir2and	|- ( ( K e. A /\ W e. H ) -> ( _I |` B ) e. D )