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	$$⊢\phi \to A\subseteq ℂ$$
	fourierdlem23.f	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
	fourierdlem23.b	$$⊢\phi \to B\subseteq ℂ$$
	fourierdlem23.x	$$⊢\phi \to X\in ℂ$$
	fourierdlem23.xps	$$⊢\left(\phi \wedge s\in B\right)\to X+s\in A$$
Assertion	fourierdlem23	$$⊢\phi \to \left(s\in B⟼F\left(X+s\right)\right):B\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem23.a	$$⊢\phi \to A\subseteq ℂ$$
2		fourierdlem23.f	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
3		fourierdlem23.b	$$⊢\phi \to B\subseteq ℂ$$
4		fourierdlem23.x	$$⊢\phi \to X\in ℂ$$
5		fourierdlem23.xps	$$⊢\left(\phi \wedge s\in B\right)\to X+s\in A$$
6		eqid	$$⊢\left(s\in B⟼X+s\right)=\left(s\in B⟼X+s\right)$$
7	6	addccncf2	$$⊢\left(B\subseteq ℂ\wedge X\in ℂ\right)\to \left(s\in B⟼X+s\right):B\underset{cn}{⟶}ℂ$$
8	3 4 7	syl2anc	$$⊢\phi \to \left(s\in B⟼X+s\right):B\underset{cn}{⟶}ℂ$$
9		ssid	$$⊢B\subseteq B$$
10	9	a1i	$$⊢\phi \to B\subseteq B$$
11	6 8 10 1 5	cncfmptssg	$$⊢\phi \to \left(s\in B⟼X+s\right):B\underset{cn}{⟶}A$$
12	11 2	cncfcompt	$$⊢\phi \to \left(s\in B⟼F\left(X+s\right)\right):B\underset{cn}{⟶}ℂ$$