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 ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II )

Proof

Step Hyp Ref Expression
1 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 dfii3 II = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) )
3 1 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4 3 a1i ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
5 unitssre ( 0 [,] 1 ) ⊆ ℝ
6 ax-resscn ℝ ⊆ ℂ
7 5 6 sstri ( 0 [,] 1 ) ⊆ ℂ
8 7 a1i ( ⊤ → ( 0 [,] 1 ) ⊆ ℂ )
9 ax-mulf · : ( ℂ × ℂ ) ⟶ ℂ
10 ffn ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
11 9 10 ax-mp · Fn ( ℂ × ℂ )
12 fnov ( · Fn ( ℂ × ℂ ) ↔ · = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) )
13 11 12 mpbi · = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) )
14 1 mulcn · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
15 13 14 eqeltrri ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
16 15 a1i ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
17 2 4 8 2 4 8 16 cnmpt2res ( ⊤ → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) )
18 17 mptru ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) )
19 iimulcl ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) )
20 19 rgen2 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 )
21 eqid ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) )
22 21 fmpo ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) )
23 frn ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
24 22 23 sylbi ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
25 20 24 ax-mp ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 )
26 cnrest2 ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) ) )
27 3 25 7 26 mp3an ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) )
28 18 27 mpbi ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
29 2 oveq2i ( ( II ×t II ) Cn II ) = ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
30 28 29 eleqtrri ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II )