Metamath Proof Explorer

Theorem gg-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 gg-iimulcn ⊢x∈01,y∈01⟼x⁢y∈II×tIICnII

Proof

Step Hyp Ref Expression
1 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
2 1 dfii3 ⊢II=TopOpen⁡ℂfld↾𝑡01
3 1 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
4 3 a1i ⊢⊤→TopOpen⁡ℂfld∈TopOn⁡ℂ
5 unitsscn ⊢01⊆ℂ
6 5 a1i ⊢⊤→01⊆ℂ
7 1 mpomulcn ⊢x∈ℂ,y∈ℂ⟼x⁢y∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
8 7 a1i ⊢⊤→x∈ℂ,y∈ℂ⟼x⁢y∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
9 2 4 6 2 4 6 8 cnmpt2res ⊢⊤→x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld
10 9 mptru ⊢x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld
11 iimulcl ⊢x∈01∧y∈01→x⁢y∈01
12 11 rgen2 ⊢∀x∈01∀y∈01x⁢y∈01
13 eqid ⊢x∈01,y∈01⟼x⁢y=x∈01,y∈01⟼x⁢y
14 13 fmpo ⊢∀x∈01∀y∈01x⁢y∈01↔x∈01,y∈01⟼x⁢y:01×01⟶01
15 frn ⊢x∈01,y∈01⟼x⁢y:01×01⟶01→ran⁡x∈01,y∈01⟼x⁢y⊆01
16 14 15 sylbi ⊢∀x∈01∀y∈01x⁢y∈01→ran⁡x∈01,y∈01⟼x⁢y⊆01
17 12 16 ax-mp ⊢ran⁡x∈01,y∈01⟼x⁢y⊆01
18 cnrest2 ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧ran⁡x∈01,y∈01⟼x⁢y⊆01∧01⊆ℂ→x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld↔x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld↾𝑡01
19 3 17 5 18 mp3an ⊢x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld↔x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld↾𝑡01
20 10 19 mpbi ⊢x∈01,y∈01⟼x⁢y∈II×tIICnTopOpen⁡ℂfld↾𝑡01
21 2 oveq2i ⊢II×tIICnII=II×tIICnTopOpen⁡ℂfld↾𝑡01
22 20 21 eleqtrri ⊢x∈01,y∈01⟼x⁢y∈II×tIICnII