Theorem ldilval

Description: Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ldilval.b	$$⊢B={\mathrm{Base}}_K$$
	ldilval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ldilval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ldilval.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
Assertion	ldilval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in D\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\to F\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		ldilval.b	$$⊢B={\mathrm{Base}}_K$$
2		ldilval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		ldilval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		ldilval.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
5		eqid	$$⊢\mathrm{LAut}\left(K\right)=\mathrm{LAut}\left(K\right)$$
6	1 2 3 5 4	isldil	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in D\leftrightarrow \left(F\in \mathrm{LAut}\left(K\right)\wedge \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)\right)$$
7		simpr	$$⊢\left(F\in \mathrm{LAut}\left(K\right)\wedge \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)\to \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)$$
8	6 7	biimtrdi	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in D\to \forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\right)$$
9		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }W\leftrightarrow X\underset{\dot{}}{\le }W\right)$$
10		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
11		id	$$⊢x=X\to x=X$$
12	10 11	eqeq12d	$$⊢x=X\to \left(F\left(x\right)=x\leftrightarrow F\left(X\right)=X\right)$$
13	9 12	imbi12d	$$⊢x=X\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)$$
14	13	rspccv	$$⊢\forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\to \left(X\in B\to \left(X\underset{\dot{}}{\le }W\to F\left(X\right)=X\right)\right)$$
15	14	impd	$$⊢\forall x\in B\left(x\underset{\dot{}}{\le }W\to F\left(x\right)=x\right)\to \left(\left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\to F\left(X\right)=X\right)$$
16	8 15	syl6	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in D\to \left(\left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\to F\left(X\right)=X\right)\right)$$
17	16	3imp	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in D\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\to F\left(X\right)=X$$