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 ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn II

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 1 dfii3 ⊢ II = TopOpen ⁡ ℂ fld ↾ 𝑡 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 ℂ × ℂ ↔ × = x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y
13 11 12 mpbi ⊢ × = x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y
14 1 mulcn ⊢ × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
15 13 14 eqeltrri ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
16 15 a1i ⊢ ⊤ → x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 2 4 8 2 4 8 16 cnmpt2res ⊢ ⊤ → x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld
18 17 mptru ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld
19 iimulcl ⊢ x ∈ 0 1 ∧ y ∈ 0 1 → x ⁢ y ∈ 0 1
20 19 rgen2 ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1
21 eqid ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y = x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y
22 21 fmpo ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1 ↔ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y : 0 1 × 0 1 ⟶ 0 1
23 frn ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y : 0 1 × 0 1 ⟶ 0 1 → ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1
24 22 23 sylbi ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1 → ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1
25 20 24 ax-mp ⊢ ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1
26 cnrest2 ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1 ∧ 0 1 ⊆ ℂ → x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↔ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
27 3 25 7 26 mp3an ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↔ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
28 18 27 mpbi ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
29 2 oveq2i ⊢ II × t II Cn II = II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
30 28 29 eleqtrri ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn II