Metamath Proof Explorer

Theorem dirkerval

Description: The N_th Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerval.1 
|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
Assertion dirkerval 
|- ( N e. NN -> ( D ` N ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkerval.1 
 |-  D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
2 simpl 
 |-  ( ( m = N /\ s e. RR ) -> m = N )
3 2 oveq2d 
 |-  ( ( m = N /\ s e. RR ) -> ( 2 x. m ) = ( 2 x. N ) )
4 3 oveq1d 
 |-  ( ( m = N /\ s e. RR ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. N ) + 1 ) )
5 4 oveq1d 
 |-  ( ( m = N /\ s e. RR ) -> ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
6 2 oveq1d 
 |-  ( ( m = N /\ s e. RR ) -> ( m + ( 1 / 2 ) ) = ( N + ( 1 / 2 ) ) )
7 6 fvoveq1d 
 |-  ( ( m = N /\ s e. RR ) -> ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
8 7 oveq1d 
 |-  ( ( m = N /\ s e. RR ) -> ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
9 5 8 ifeq12d 
 |-  ( ( m = N /\ s e. RR ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
10 9 mpteq2dva 
 |-  ( m = N -> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
11 simpl 
 |-  ( ( n = m /\ s e. RR ) -> n = m )
12 11 oveq2d 
 |-  ( ( n = m /\ s e. RR ) -> ( 2 x. n ) = ( 2 x. m ) )
13 12 oveq1d 
 |-  ( ( n = m /\ s e. RR ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. m ) + 1 ) )
14 13 oveq1d 
 |-  ( ( n = m /\ s e. RR ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) )
15 11 oveq1d 
 |-  ( ( n = m /\ s e. RR ) -> ( n + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
16 15 fvoveq1d 
 |-  ( ( n = m /\ s e. RR ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) )
17 16 oveq1d 
 |-  ( ( n = m /\ s e. RR ) -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
18 14 17 ifeq12d 
 |-  ( ( n = m /\ s e. RR ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
19 18 mpteq2dva 
 |-  ( n = m -> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
20 19 cbvmptv 
 |-  ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) ) = ( m e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
21 1 20 eqtri 
 |-  D = ( m e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
22 reex 
 |-  RR e. _V
23 22 mptex 
 |-  ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) e. _V
24 10 21 23 fvmpt 
 |-  ( N e. NN -> ( D ` N ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )