Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldilcnv Structured version   Unicode version

Theorem ldilcnv 30986
 Description: The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.)
Hypotheses
Ref Expression
ldilcnv.h
ldilcnv.d
Assertion
Ref Expression
ldilcnv

Proof of Theorem ldilcnv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpll 732 . . 3
2 ldilcnv.h . . . 4
3 eqid 2438 . . . 4
4 ldilcnv.d . . . 4
52, 3, 4ldillaut 30982 . . 3
63lautcnv 30961 . . 3
71, 5, 6syl2anc 644 . 2
8 eqid 2438 . . . . . . . . 9
9 eqid 2438 . . . . . . . . 9
108, 9, 2, 4ldilval 30984 . . . . . . . 8
11103expa 1154 . . . . . . 7
12113impb 1150 . . . . . 6
1312fveq2d 5735 . . . . 5
148, 2, 4ldil1o 30983 . . . . . . 7
15143ad2ant1 979 . . . . . 6
16 simp2 959 . . . . . 6
17 f1ocnvfv1 6017 . . . . . 6
1815, 16, 17syl2anc 644 . . . . 5
1913, 18eqtr3d 2472 . . . 4
20193exp 1153 . . 3
2120ralrimiv 2790 . 2
228, 9, 2, 3, 4isldil 30981 . . 3