Theorem fourierdlem23

Description: If F is continuous and X is constant, then ( F( X + s ) ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem23.a	|- ( ph -> A C_ CC )
	fourierdlem23.f	|- ( ph -> F e. ( A -cn-> CC ) )
	fourierdlem23.b	|- ( ph -> B C_ CC )
	fourierdlem23.x	|- ( ph -> X e. CC )
	fourierdlem23.xps	|- ( ( ph /\ s e. B ) -> ( X + s ) e. A )
Assertion	fourierdlem23	|- ( ph -> ( s e. B |-> ( F ` ( X + s ) ) ) e. ( B -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem23.a	|- ( ph -> A C_ CC )
2		fourierdlem23.f	|- ( ph -> F e. ( A -cn-> CC ) )
3		fourierdlem23.b	|- ( ph -> B C_ CC )
4		fourierdlem23.x	|- ( ph -> X e. CC )
5		fourierdlem23.xps	|- ( ( ph /\ s e. B ) -> ( X + s ) e. A )
6		eqid	|- ( s e. B |-> ( X + s ) ) = ( s e. B |-> ( X + s ) )
7	6	addccncf2	|- ( ( B C_ CC /\ X e. CC ) -> ( s e. B |-> ( X + s ) ) e. ( B -cn-> CC ) )
8	3 4 7	syl2anc	|- ( ph -> ( s e. B |-> ( X + s ) ) e. ( B -cn-> CC ) )
9		ssid	|- B C_ B
10	9	a1i	|- ( ph -> B C_ B )
11	6 8 10 1 5	cncfmptssg	|- ( ph -> ( s e. B |-> ( X + s ) ) e. ( B -cn-> A ) )
12	11 2	cncfcompt	|- ( ph -> ( s e. B |-> ( F ` ( X + s ) ) ) e. ( B -cn-> CC ) )