Theorem idldil

Description: The identity function is a lattice dilation. (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	idldil.b	$$⊢B={\mathrm{Base}}_K$$
	idldil.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	idldil.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
Assertion	idldil	$$⊢\left(K\in A\wedge W\in H\right)\to {\mathrm{I}\upharpoonright }_B\in D$$

Proof

Step	Hyp	Ref	Expression
1		idldil.b	$$⊢B={\mathrm{Base}}_K$$
2		idldil.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		idldil.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
4		eqid	$$⊢\mathrm{LAut}\left(K\right)=\mathrm{LAut}\left(K\right)$$
5	1 4	idlaut	$$⊢K\in A\to {\mathrm{I}\upharpoonright }_B\in \mathrm{LAut}\left(K\right)$$
6	5	adantr	$$⊢\left(K\in A\wedge W\in H\right)\to {\mathrm{I}\upharpoonright }_B\in \mathrm{LAut}\left(K\right)$$
7		fvresi	$$⊢x\in B\to \left({\mathrm{I}\upharpoonright }_B\right)\left(x\right)=x$$
8	7	a1d	$$⊢x\in B\to \left(x{\le }_{K}W\to \left({\mathrm{I}\upharpoonright }_B\right)\left(x\right)=x\right)$$
9	8	rgen	$$⊢\forall x\in B\left(x{\le }_{K}W\to \left({\mathrm{I}\upharpoonright }_B\right)\left(x\right)=x\right)$$
10	9	a1i	$$⊢\left(K\in A\wedge W\in H\right)\to \forall x\in B\left(x{\le }_{K}W\to \left({\mathrm{I}\upharpoonright }_B\right)\left(x\right)=x\right)$$
11		eqid	$$⊢{\le }_K={\le }_K$$
12	1 11 2 4 3	isldil	$$⊢\left(K\in A\wedge W\in H\right)\to \left({\mathrm{I}\upharpoonright }_B\in D\leftrightarrow \left({\mathrm{I}\upharpoonright }_B\in \mathrm{LAut}\left(K\right)\wedge \forall x\in B\left(x{\le }_{K}W\to \left({\mathrm{I}\upharpoonright }_B\right)\left(x\right)=x\right)\right)\right)$$
13	6 10 12	mpbir2and	$$⊢\left(K\in A\wedge W\in H\right)\to {\mathrm{I}\upharpoonright }_B\in D$$