This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )