Metamath Proof Explorer

Theorem dilfsetN

Description: The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-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 dilfsetN 
|- ( K e. B -> L = ( d e. A |-> { 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 elex 
 |-  ( K e. B -> K e. _V )
7 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
8 7 1 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
9 fveq2 
 |-  ( k = K -> ( PAut ` k ) = ( PAut ` K ) )
10 9 4 eqtr4di 
 |-  ( k = K -> ( PAut ` k ) = M )
11 fveq2 
 |-  ( k = K -> ( PSubSp ` k ) = ( PSubSp ` K ) )
12 11 2 eqtr4di 
 |-  ( k = K -> ( PSubSp ` k ) = S )
13 fveq2 
 |-  ( k = K -> ( WAtoms ` k ) = ( WAtoms ` K ) )
14 13 3 eqtr4di 
 |-  ( k = K -> ( WAtoms ` k ) = W )
15 14 fveq1d 
 |-  ( k = K -> ( ( WAtoms ` k ) ` d ) = ( W ` d ) )
16 15 sseq2d 
 |-  ( k = K -> ( x C_ ( ( WAtoms ` k ) ` d ) <-> x C_ ( W ` d ) ) )
17 16 imbi1d 
 |-  ( k = K -> ( ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) <-> ( x C_ ( W ` d ) -> ( f ` x ) = x ) ) )
18 12 17 raleqbidv 
 |-  ( k = K -> ( A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) <-> A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) ) )
19 10 18 rabeqbidv 
 |-  ( k = K -> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } = { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } )
20 8 19 mpteq12dv 
 |-  ( k = K -> ( d e. ( Atoms ` k ) |-> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } ) = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )
21 df-dilN 
 |-  Dil = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } ) )
22 20 21 1 mptfvmpt 
 |-  ( K e. _V -> ( Dil ` K ) = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )
23 5 22 syl5eq 
 |-  ( K e. _V -> L = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )
24 6 23 syl 
 |-  ( K e. B -> L = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )