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 = ( Base ` K )
	ldilset.l	|- .<_ = ( le ` K )
	ldilset.h	|- H = ( LHyp ` K )
	ldilset.i	|- I = ( LAut ` K )
	ldilset.d	|- D = ( ( LDil ` K ) ` W )
Assertion	ldilset	|- ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )

Proof

Step	Hyp	Ref	Expression
1		ldilset.b	|- B = ( Base ` K )
2		ldilset.l	|- .<_ = ( le ` K )
3		ldilset.h	|- H = ( LHyp ` K )
4		ldilset.i	|- I = ( LAut ` K )
5		ldilset.d	|- D = ( ( LDil ` K ) ` W )
6	1 2 3 4	ldilfset	|- ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )
7	6	fveq1d	|- ( K e. C -> ( ( LDil ` K ) ` W ) = ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) )
8		breq2	|- ( w = W -> ( x .<_ w <-> x .<_ W ) )
9	8	imbi1d	|- ( w = W -> ( ( x .<_ w -> ( f ` x ) = x ) <-> ( x .<_ W -> ( f ` x ) = x ) ) )
10	9	ralbidv	|- ( w = W -> ( A. x e. B ( x .<_ w -> ( f ` x ) = x ) <-> A. x e. B ( x .<_ W -> ( f ` x ) = x ) ) )
11	10	rabbidv	|- ( w = W -> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
12		eqid	|- ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } )
13	4	fvexi	|- I e. _V
14	13	rabex	|- { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } e. _V
15	11 12 14	fvmpt	|- ( W e. H -> ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
16	7 15	sylan9eq	|- ( ( K e. C /\ W e. H ) -> ( ( LDil ` K ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
17	5 16	eqtrid	|- ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )