Metamath Proof Explorer

Theorem trnsetN

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

Ref Expression
Hypotheses trnset.a 
|- A = ( Atoms ` K )
trnset.s 
|- S = ( PSubSp ` K )
trnset.p 
|- .+ = ( +P ` K )
trnset.o 
|- ._|_ = ( _|_P ` K )
trnset.w 
|- W = ( WAtoms ` K )
trnset.m 
|- M = ( PAut ` K )
trnset.l 
|- L = ( Dil ` K )
trnset.t 
|- T = ( Trn ` K )
Assertion trnsetN 
|- ( ( K e. B /\ D e. A ) -> ( T ` D ) = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )

Proof

Step Hyp Ref Expression
1 trnset.a 
 |-  A = ( Atoms ` K )
2 trnset.s 
 |-  S = ( PSubSp ` K )
3 trnset.p 
 |-  .+ = ( +P ` K )
4 trnset.o 
 |-  ._|_ = ( _|_P ` K )
5 trnset.w 
 |-  W = ( WAtoms ` K )
6 trnset.m 
 |-  M = ( PAut ` K )
7 trnset.l 
 |-  L = ( Dil ` K )
8 trnset.t 
 |-  T = ( Trn ` K )
9 1 2 3 4 5 6 7 8 trnfsetN 
 |-  ( K e. B -> T = ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } ) )
10 9 fveq1d 
 |-  ( K e. B -> ( T ` D ) = ( ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } ) ` D ) )
11 fveq2 
 |-  ( d = D -> ( L ` d ) = ( L ` D ) )
12 fveq2 
 |-  ( d = D -> ( W ` d ) = ( W ` D ) )
13 sneq 
 |-  ( d = D -> { d } = { D } )
14 13 fveq2d 
 |-  ( d = D -> ( ._|_ ` { d } ) = ( ._|_ ` { D } ) )
15 14 ineq2d 
 |-  ( d = D -> ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) )
16 14 ineq2d 
 |-  ( d = D -> ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) )
17 15 16 eqeq12d 
 |-  ( d = D -> ( ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) <-> ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
18 12 17 raleqbidv 
 |-  ( d = D -> ( A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) <-> A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
19 12 18 raleqbidv 
 |-  ( d = D -> ( A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) <-> A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) ) )
20 11 19 rabeqbidv 
 |-  ( d = D -> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )
21 eqid 
 |-  ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } ) = ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } )
22 fvex 
 |-  ( L ` D ) e. _V
23 22 rabex 
 |-  { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } e. _V
24 20 21 23 fvmpt 
 |-  ( D e. A -> ( ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } ) ` D ) = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )
25 10 24 sylan9eq 
 |-  ( ( K e. B /\ D e. A ) -> ( T ` D ) = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )