# Metamath Proof Explorer

Description: Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis addccncf.1 ${⊢}{F}=\left({x}\in ℂ⟼{x}+{A}\right)$
Assertion addccncf ${⊢}{A}\in ℂ\to {F}:ℂ\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 addccncf.1 ${⊢}{F}=\left({x}\in ℂ⟼{x}+{A}\right)$
2 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 2 addcn ${⊢}+\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
4 3 a1i ${⊢}{A}\in ℂ\to +\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
5 ssid ${⊢}ℂ\subseteq ℂ$
6 cncfmptid ${⊢}\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
7 5 5 6 mp2an ${⊢}\left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
8 7 a1i ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
9 cncfmptc ${⊢}\left({A}\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in ℂ⟼{A}\right):ℂ\underset{cn}{⟶}ℂ$
10 5 5 9 mp3an23 ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{A}\right):ℂ\underset{cn}{⟶}ℂ$
11 2 4 8 10 cncfmpt2f ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{x}+{A}\right):ℂ\underset{cn}{⟶}ℂ$
12 1 11 eqeltrid ${⊢}{A}\in ℂ\to {F}:ℂ\underset{cn}{⟶}ℂ$