Metamath Proof Explorer


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