Theorem ldilset

Description: The set of lattice dilations for a fiducial co-atom W . (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	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\}$$

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	ldilfset	$$⊢K\in C\to \mathrm{LDil}\left(K\right)=\left(w\in H⟼\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}\right)$$
7	6	fveq1d	$$⊢K\in C\to \mathrm{LDil}\left(K\right)\left(W\right)=\left(w\in H⟼\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}\right)\left(W\right)$$
8		breq2	$$⊢w=W\to \left(x\underset{\dot{}}{\le }w\leftrightarrow x\underset{\dot{}}{\le }W\right)$$
9	8	imbi1d	$$⊢w=W\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)$$
10	9	ralbidv	$$⊢w=W\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)$$
11	10	rabbidv	$$⊢w=W\to \left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}=\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}$$
12		eqid	$$⊢\left(w\in H⟼\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}\right)=\left(w\in H⟼\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}\right)$$
13	4	fvexi	$$⊢I\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}\in \mathrm{V}$$
15	11 12 14	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }w\to f\left(x\right)=x\right)\right\}\right)\left(W\right)=\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}$$
16	7 15	sylan9eq	$$⊢\left(K\in C\wedge W\in H\right)\to \mathrm{LDil}\left(K\right)\left(W\right)=\left\{f\in I|\forall x\in B\left(x\underset{\dot{}}{\le }W\to f\left(x\right)=x\right)\right\}$$
17	5 16	syl5eq	$$⊢\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\}$$