Theorem dilsetN

Description: The set of dilations for a fiducial atom D . (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dilset.a	|- A = ( Atoms ` K )
	dilset.s	|- S = ( PSubSp ` K )
	dilset.w	|- W = ( WAtoms ` K )
	dilset.m	|- M = ( PAut ` K )
	dilset.l	|- L = ( Dil ` K )
Assertion	dilsetN	|- ( ( K e. B /\ D e. A ) -> ( L ` D ) = { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } )

Proof

Step	Hyp	Ref	Expression
1		dilset.a	|- A = ( Atoms ` K )
2		dilset.s	|- S = ( PSubSp ` K )
3		dilset.w	|- W = ( WAtoms ` K )
4		dilset.m	|- M = ( PAut ` K )
5		dilset.l	|- L = ( Dil ` K )
6	1 2 3 4 5	dilfsetN	|- ( K e. B -> L = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )
7	6	fveq1d	|- ( K e. B -> ( L ` D ) = ( ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) ` D ) )
8		fveq2	|- ( d = D -> ( W ` d ) = ( W ` D ) )
9	8	sseq2d	|- ( d = D -> ( x C_ ( W ` d ) <-> x C_ ( W ` D ) ) )
10	9	imbi1d	|- ( d = D -> ( ( x C_ ( W ` d ) -> ( f ` x ) = x ) <-> ( x C_ ( W ` D ) -> ( f ` x ) = x ) ) )
11	10	ralbidv	|- ( d = D -> ( A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) <-> A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) ) )
12	11	rabbidv	|- ( d = D -> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } = { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } )
13		eqid	|- ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } )
14	4	fvexi	|- M e. _V
15	14	rabex	|- { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } e. _V
16	12 13 15	fvmpt	|- ( D e. A -> ( ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) ` D ) = { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } )
17	7 16	sylan9eq	|- ( ( K e. B /\ D e. A ) -> ( L ` D ) = { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } )