# Metamath Proof Explorer

## Theorem iimulcn

Description: Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014)

Ref Expression
Assertion iimulcn ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 1 dfii3 ${⊢}\mathrm{II}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right]$
3 1 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
4 3 a1i ${⊢}\top \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
5 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
6 ax-resscn ${⊢}ℝ\subseteq ℂ$
7 5 6 sstri ${⊢}\left[0,1\right]\subseteq ℂ$
8 7 a1i ${⊢}\top \to \left[0,1\right]\subseteq ℂ$
9 ax-mulf ${⊢}×:ℂ×ℂ⟶ℂ$
10 ffn ${⊢}×:ℂ×ℂ⟶ℂ\to ×Fn\left(ℂ×ℂ\right)$
11 9 10 ax-mp ${⊢}×Fn\left(ℂ×ℂ\right)$
12 fnov ${⊢}×Fn\left(ℂ×ℂ\right)↔×=\left({x}\in ℂ,{y}\in ℂ⟼{x}{y}\right)$
13 11 12 mpbi ${⊢}×=\left({x}\in ℂ,{y}\in ℂ⟼{x}{y}\right)$
14 1 mulcn ${⊢}×\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)$
15 13 14 eqeltrri ${⊢}\left({x}\in ℂ,{y}\in ℂ⟼{x}{y}\right)\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)$
16 15 a1i ${⊢}\top \to \left({x}\in ℂ,{y}\in ℂ⟼{x}{y}\right)\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)$
17 2 4 8 2 4 8 16 cnmpt2res ${⊢}\top \to \left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
18 17 mptru ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
19 iimulcl ${⊢}\left({x}\in \left[0,1\right]\wedge {y}\in \left[0,1\right]\right)\to {x}{y}\in \left[0,1\right]$
20 19 rgen2 ${⊢}\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{x}{y}\in \left[0,1\right]$
21 eqid ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)$
22 21 fmpo ${⊢}\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{x}{y}\in \left[0,1\right]↔\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right):\left[0,1\right]×\left[0,1\right]⟶\left[0,1\right]$
23 frn ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right):\left[0,1\right]×\left[0,1\right]⟶\left[0,1\right]\to \mathrm{ran}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\subseteq \left[0,1\right]$
24 22 23 sylbi ${⊢}\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{x}{y}\in \left[0,1\right]\to \mathrm{ran}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\subseteq \left[0,1\right]$
25 20 24 ax-mp ${⊢}\mathrm{ran}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\subseteq \left[0,1\right]$
26 cnrest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq ℂ\right)\to \left(\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right]\right)\right)\right)$
27 3 25 7 26 mp3an ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)↔\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right]\right)\right)$
28 18 27 mpbi ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right]\right)\right)$
29 2 oveq2i ${⊢}\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}=\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}\left[0,1\right]\right)$
30 28 29 eleqtrri ${⊢}\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼{x}{y}\right)\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}\mathrm{II}\right)$