Metamath Proof Explorer

Theorem trnfsetN

Description: The mapping from fiducial atom to set of translations. (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 trnfsetN 
|- ( K e. C -> 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 } ) ) } ) )

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 elex 
 |-  ( K e. C -> K e. _V )
10 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
11 10 1 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
12 fveq2 
 |-  ( k = K -> ( Dil ` k ) = ( Dil ` K ) )
13 12 7 eqtr4di 
 |-  ( k = K -> ( Dil ` k ) = L )
14 13 fveq1d 
 |-  ( k = K -> ( ( Dil ` k ) ` d ) = ( L ` d ) )
15 fveq2 
 |-  ( k = K -> ( WAtoms ` k ) = ( WAtoms ` K ) )
16 15 5 eqtr4di 
 |-  ( k = K -> ( WAtoms ` k ) = W )
17 16 fveq1d 
 |-  ( k = K -> ( ( WAtoms ` k ) ` d ) = ( W ` d ) )
18 fveq2 
 |-  ( k = K -> ( +P ` k ) = ( +P ` K ) )
19 18 3 eqtr4di 
 |-  ( k = K -> ( +P ` k ) = .+ )
20 19 oveqd 
 |-  ( k = K -> ( q ( +P ` k ) ( f ` q ) ) = ( q .+ ( f ` q ) ) )
21 fveq2 
 |-  ( k = K -> ( _|_P ` k ) = ( _|_P ` K ) )
22 21 4 eqtr4di 
 |-  ( k = K -> ( _|_P ` k ) = ._|_ )
23 22 fveq1d 
 |-  ( k = K -> ( ( _|_P ` k ) ` { d } ) = ( ._|_ ` { d } ) )
24 20 23 ineq12d 
 |-  ( k = K -> ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) )
25 19 oveqd 
 |-  ( k = K -> ( r ( +P ` k ) ( f ` r ) ) = ( r .+ ( f ` r ) ) )
26 25 23 ineq12d 
 |-  ( k = K -> ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) )
27 24 26 eqeq12d 
 |-  ( k = K -> ( ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) <-> ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) ) )
28 17 27 raleqbidv 
 |-  ( k = K -> ( A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) <-> A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) ) )
29 17 28 raleqbidv 
 |-  ( k = K -> ( A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) <-> A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) ) )
30 14 29 rabeqbidv 
 |-  ( k = K -> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { 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 } ) ) } )
31 11 30 mpteq12dv 
 |-  ( k = K -> ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { 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 } ) ) } ) )
32 df-trnN 
 |-  Trn = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } ) )
33 31 32 1 mptfvmpt 
 |-  ( K e. _V -> ( Trn ` K ) = ( 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 } ) ) } ) )
34 8 33 syl5eq 
 |-  ( K e. _V -> 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 } ) ) } ) )
35 9 34 syl 
 |-  ( K e. C -> 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 } ) ) } ) )