Metamath Proof Explorer

Theorem vtsval

Description: Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses vtsval.n 
|- ( ph -> N e. NN0 )
vtsval.x 
|- ( ph -> X e. CC )
vtsval.l 
|- ( ph -> L : NN --> CC )
Assertion vtsval 
|- ( ph -> ( ( L vts N ) ` X ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 vtsval.n 
 |-  ( ph -> N e. NN0 )
2 vtsval.x 
 |-  ( ph -> X e. CC )
3 vtsval.l 
 |-  ( ph -> L : NN --> CC )
4 cnex 
 |-  CC e. _V
5 nnex 
 |-  NN e. _V
6 4 5 elmap 
 |-  ( L e. ( CC ^m NN ) <-> L : NN --> CC )
7 3 6 sylibr 
 |-  ( ph -> L e. ( CC ^m NN ) )
8 fveq1 
 |-  ( l = L -> ( l ` a ) = ( L ` a ) )
9 8 oveq1d 
 |-  ( l = L -> ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) )
10 9 sumeq2sdv 
 |-  ( l = L -> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = sum_ a e. ( 1 ... n ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) )
11 10 mpteq2dv 
 |-  ( l = L -> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) = ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
12 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
13 12 sumeq1d 
 |-  ( n = N -> sum_ a e. ( 1 ... n ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) )
14 13 mpteq2dv 
 |-  ( n = N -> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) = ( x e. CC |-> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
15 df-vts 
 |-  vts = ( l e. ( CC ^m NN ) , n e. NN0 |-> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
16 4 mptex 
 |-  ( x e. CC |-> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) e. _V
17 11 14 15 16 ovmpo 
 |-  ( ( L e. ( CC ^m NN ) /\ N e. NN0 ) -> ( L vts N ) = ( x e. CC |-> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
18 7 1 17 syl2anc 
 |-  ( ph -> ( L vts N ) = ( x e. CC |-> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
19 oveq2 
 |-  ( x = X -> ( a x. x ) = ( a x. X ) )
20 19 oveq2d 
 |-  ( x = X -> ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) )
21 20 fveq2d 
 |-  ( x = X -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) )
22 21 oveq2d 
 |-  ( x = X -> ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )
23 22 sumeq2sdv 
 |-  ( x = X -> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )
24 23 adantl 
 |-  ( ( ph /\ x = X ) -> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )
25 sumex 
 |-  sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) e. _V
26 25 a1i 
 |-  ( ph -> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) e. _V )
27 18 24 2 26 fvmptd 
 |-  ( ph -> ( ( L vts N ) ` X ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )