Theorem addccncf2

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

	Ref	Expression
Hypothesis	addccncf2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) )
Assertion	addccncf2	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		addccncf2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) )
2		simpl	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ⊆ ℂ )
3		simpr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
4		ssidd	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ℂ ⊆ ℂ )
5	2 3 4	constcncfg	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
6		ssid	⊢ ℂ ⊆ ℂ
7		cncfmptid	⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
8	6 7	mpan2	⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
9	8	adantr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
10	5 9	addcncf	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
11	1 10	eqeltrid	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )