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 φ A
fourierdlem23.f φ F : A cn
fourierdlem23.b φ B
fourierdlem23.x φ X
fourierdlem23.xps φ s B X + s A
Assertion fourierdlem23 φ s B F X + s : B cn

Proof

Step Hyp Ref Expression
1 fourierdlem23.a φ A
2 fourierdlem23.f φ F : A cn
3 fourierdlem23.b φ B
4 fourierdlem23.x φ X
5 fourierdlem23.xps φ s B X + s A
6 eqid s B X + s = s B X + s
7 6 addccncf2 B X s B X + s : B cn
8 3 4 7 syl2anc φ s B X + s : B cn
9 ssid B B
10 9 a1i φ B B
11 6 8 10 1 5 cncfmptssg φ s B X + s : B cn A
12 11 2 cncfcompt φ s B F X + s : B cn