Metamath Proof Explorer

Theorem iimulcn

Description: Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 unitsscn ⊢ 0 1 ⊆ ℂ
6 5 a1i ⊢ ⊤ → 0 1 ⊆ ℂ
7 1 mpomulcn ⊢ x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
8 7 a1i ⊢ ⊤ → x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
9 2 4 6 2 4 6 8 cnmpt2res ⊢ ⊤ → x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld
10 9 mptru ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld
11 iimulcl ⊢ x ∈ 0 1 ∧ y ∈ 0 1 → x ⁢ y ∈ 0 1
12 11 rgen2 ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1
13 eqid ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y = x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y
14 13 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
15 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
16 14 15 sylbi ⊢ ∀ x ∈ 0 1 ∀ y ∈ 0 1 x ⁢ y ∈ 0 1 → ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1
17 12 16 ax-mp ⊢ ran ⁡ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ⊆ 0 1
18 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
19 3 17 5 18 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
20 10 19 mpbi ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
21 2 oveq2i ⊢ II × t II Cn II = II × t II Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 1
22 20 21 eleqtrri ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ x ⁢ y ∈ II × t II Cn II