Metamath Proof Explorer

Theorem ldilcnv

Description: The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013)

Ref Expression
Hypotheses ldilcnv.h 
|- H = ( LHyp ` K )
ldilcnv.d 
|- D = ( ( LDil ` K ) ` W )
Assertion ldilcnv 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> `' F e. D )

Proof

Step Hyp Ref Expression
1 ldilcnv.h 
 |-  H = ( LHyp ` K )
2 ldilcnv.d 
 |-  D = ( ( LDil ` K ) ` W )
3 simpll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> K e. HL )
4 eqid 
 |-  ( LAut ` K ) = ( LAut ` K )
5 1 4 2 ldillaut 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> F e. ( LAut ` K ) )
6 4 lautcnv 
 |-  ( ( K e. HL /\ F e. ( LAut ` K ) ) -> `' F e. ( LAut ` K ) )
7 3 5 6 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> `' F e. ( LAut ` K ) )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 8 9 1 2 ldilval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( F ` x ) = x )
11 10 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( F ` x ) = x )
12 11 3impb 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( F ` x ) = x )
13 12 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( `' F ` ( F ` x ) ) = ( `' F ` x ) )
14 8 1 2 ldil1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
15 14 3ad2ant1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
16 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> x e. ( Base ` K ) )
17 f1ocnvfv1 
 |-  ( ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( `' F ` ( F ` x ) ) = x )
18 15 16 17 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( `' F ` ( F ` x ) ) = x )
19 13 18 eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( `' F ` x ) = x )
20 19 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> ( x e. ( Base ` K ) -> ( x ( le ` K ) W -> ( `' F ` x ) = x ) ) )
21 20 ralrimiv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( `' F ` x ) = x ) )
22 8 9 1 4 2 isldil 
 |-  ( ( K e. HL /\ W e. H ) -> ( `' F e. D <-> ( `' F e. ( LAut ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( `' F ` x ) = x ) ) ) )
23 22 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> ( `' F e. D <-> ( `' F e. ( LAut ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( `' F ` x ) = x ) ) ) )
24 7 21 23 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> `' F e. D )