Theorem fourierdlem67

Description: G is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem67.f	|- ( ph -> F : RR --> RR )
	fourierdlem67.x	|- ( ph -> X e. RR )
	fourierdlem67.y	|- ( ph -> Y e. RR )
	fourierdlem67.w	|- ( ph -> W e. RR )
	fourierdlem67.h	|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
	fourierdlem67.k	|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
	fourierdlem67.u	|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
	fourierdlem67.n	|- ( ph -> N e. RR )
	fourierdlem67.s	|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
	fourierdlem67.g	|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
Assertion	fourierdlem67	|- ( ph -> G : ( -u _pi [,] _pi ) --> RR )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem67.f	|- ( ph -> F : RR --> RR )
2		fourierdlem67.x	|- ( ph -> X e. RR )
3		fourierdlem67.y	|- ( ph -> Y e. RR )
4		fourierdlem67.w	|- ( ph -> W e. RR )
5		fourierdlem67.h	|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
6		fourierdlem67.k	|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
7		fourierdlem67.u	|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
8		fourierdlem67.n	|- ( ph -> N e. RR )
9		fourierdlem67.s	|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
10		fourierdlem67.g	|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
11	1 2 3 4 5 6 7	fourierdlem55	|- ( ph -> U : ( -u _pi [,] _pi ) --> RR )
12	11	ffvelrnda	|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( U ` s ) e. RR )
13	9	fourierdlem5	|- ( N e. RR -> S : ( -u _pi [,] _pi ) --> RR )
14	8 13	syl	|- ( ph -> S : ( -u _pi [,] _pi ) --> RR )
15	14	ffvelrnda	|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( S ` s ) e. RR )
16	12 15	remulcld	|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( ( U ` s ) x. ( S ` s ) ) e. RR )
17	16 10	fmptd	|- ( ph -> G : ( -u _pi [,] _pi ) --> RR )