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=BaseK
idldil.h H=LHypK
idldil.d D=LDilKW
Assertion idldil KAWHIBD

Proof

Step Hyp Ref Expression
1 idldil.b B=BaseK
2 idldil.h H=LHypK
3 idldil.d D=LDilKW
4 eqid LAutK=LAutK
5 1 4 idlaut KAIBLAutK
6 5 adantr KAWHIBLAutK
7 fvresi xBIBx=x
8 7 a1d xBxKWIBx=x
9 8 rgen xBxKWIBx=x
10 9 a1i KAWHxBxKWIBx=x
11 eqid K=K
12 1 11 2 4 3 isldil KAWHIBDIBLAutKxBxKWIBx=x
13 6 10 12 mpbir2and KAWHIBD