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 HL W H F D F -1 D

Proof

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