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

Metamath Proof Explorer

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 )