Theorem isldil

Description: The predicate "is a lattice dilation". Similar to definition of dilation in Crawley p. 111. (Contributed by NM, 11-May-2012)

	Ref	Expression
Hypotheses	ldilset.b	$$⊢B={\mathrm{Base}}_K$$
	ldilset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ldilset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ldilset.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
	ldilset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
Assertion	isldil	$$⊢\left(K\in C\wedge W\in H\right)\to \left(F\in D\leftrightarrow \left(F\in I\wedge \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldilset.b	$$⊢B={\mathrm{Base}}_K$$
2		ldilset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		ldilset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		ldilset.i	$$⊢I=\mathrm{LAut}\left(K\right)$$
5		ldilset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
6	1 2 3 4 5	ldilset	$$⊢\left(K\in C\wedge W\in H\right)\to D=\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}$$
7	6	eleq2d	$$⊢\left(K\in C\wedge W\in H\right)\to \left(F\in D\leftrightarrow F\in \left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}\right)$$
8		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
9	8	eqeq1d	$$⊢f=F\to \left(f\left(x\right)=x\leftrightarrow F\left(x\right)=x\right)$$
10	9	imbi2d	$$⊢f=F\to \left(\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\leftrightarrow \left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)$$
11	10	ralbidv	$$⊢f=F\to \left(\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\leftrightarrow \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)$$
12	11	elrab	$$⊢F\in \left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}\leftrightarrow \left(F\in I\wedge \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)$$
13	7 12	bitrdi	$$⊢\left(K\in C\wedge W\in H\right)\to \left(F\in D\leftrightarrow \left(F\in I\wedge \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)\right)$$