# Metamath Proof Explorer

Description: Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis raddcn.1 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
Assertion raddcn ${⊢}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$

### Proof

Step Hyp Ref Expression
1 raddcn.1 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\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 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 xpss12 ${⊢}\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^{2}\subseteq ℂ×ℂ$
6 4 4 5 mp2an ${⊢}{ℝ}^{2}\subseteq ℂ×ℂ$
7 2 cnfldtop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
8 2 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
9 8 toponunii ${⊢}ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
10 7 7 9 9 txunii ${⊢}ℂ×ℂ=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
11 10 cnrest ${⊢}\left(+\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)\wedge {ℝ}^{2}\subseteq ℂ×ℂ\right)\to {+↾}_{{ℝ}^{2}}\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
12 3 6 11 mp2an ${⊢}{+↾}_{{ℝ}^{2}}\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
13 reex ${⊢}ℝ\in \mathrm{V}$
14 txrest ${⊢}\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\right)\wedge \left(ℝ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\right)\to \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
15 7 7 13 13 14 mp4an ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
16 2 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
17 1 16 eqtr2i ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ={J}$
18 17 17 oveq12i ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right){×}_{t}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)={J}{×}_{t}{J}$
19 15 18 eqtri ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}={J}{×}_{t}{J}$
20 19 oveq1i ${⊢}\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){↾}_{𝑡}{ℝ}^{2}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\left({J}{×}_{t}{J}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
21 12 20 eleqtri ${⊢}{+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
22 ax-addf ${⊢}+:ℂ×ℂ⟶ℂ$
23 ffn ${⊢}+:ℂ×ℂ⟶ℂ\to +Fn\left(ℂ×ℂ\right)$
24 22 23 ax-mp ${⊢}+Fn\left(ℂ×ℂ\right)$
25 fnssres ${⊢}\left(+Fn\left(ℂ×ℂ\right)\wedge {ℝ}^{2}\subseteq ℂ×ℂ\right)\to \left({+↾}_{{ℝ}^{2}}\right)Fn{ℝ}^{2}$
26 24 6 25 mp2an ${⊢}\left({+↾}_{{ℝ}^{2}}\right)Fn{ℝ}^{2}$
27 fnov ${⊢}\left({+↾}_{{ℝ}^{2}}\right)Fn{ℝ}^{2}↔{+↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼{x}\left({+↾}_{{ℝ}^{2}}\right){y}\right)$
28 26 27 mpbi ${⊢}{+↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼{x}\left({+↾}_{{ℝ}^{2}}\right){y}\right)$
29 ovres ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}\left({+↾}_{{ℝ}^{2}}\right){y}={x}+{y}$
30 29 mpoeq3ia ${⊢}\left({x}\in ℝ,{y}\in ℝ⟼{x}\left({+↾}_{{ℝ}^{2}}\right){y}\right)=\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)$
31 28 30 eqtri ${⊢}{+↾}_{{ℝ}^{2}}=\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)$
32 31 rneqi ${⊢}\mathrm{ran}\left({+↾}_{{ℝ}^{2}}\right)=\mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)$
33 readdcl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}+{y}\in ℝ$
34 33 rgen2a ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}{x}+{y}\in ℝ$
35 eqid ${⊢}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)=\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)$
36 35 rnmposs ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℝ\phantom{\rule{.4em}{0ex}}{x}+{y}\in ℝ\to \mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)\subseteq ℝ$
37 34 36 ax-mp ${⊢}\mathrm{ran}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)\subseteq ℝ$
38 32 37 eqsstri ${⊢}\mathrm{ran}\left({+↾}_{{ℝ}^{2}}\right)\subseteq ℝ$
39 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({+↾}_{{ℝ}^{2}}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left({+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔{+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\right)$
40 8 38 4 39 mp3an ${⊢}{+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔{+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
41 21 40 mpbi ${⊢}{+↾}_{{ℝ}^{2}}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)$
42 17 oveq2i ${⊢}\left({J}{×}_{t}{J}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)=\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}$
43 41 31 42 3eltr3i ${⊢}\left({x}\in ℝ,{y}\in ℝ⟼{x}+{y}\right)\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$