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	⊢ ( 𝑥 ∈ ( 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		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
6	5	a1i	⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℂ )
7	1	mpomulcn	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
8	7	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
9	2 4 6 2 4 6 8	cnmpt2res	⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) )
10	9	mptru	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) )
11		iimulcl	⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) )
12	11	rgen2	⊢ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 )
13		eqid	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) )
14	13	fmpo	⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) )
15		frn	⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
16	14 15	sylbi	⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
17	12 16	ax-mp	⊢ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 )
18		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 ) ) ) ) )
19	3 17 5 18	mp3an	⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) )
20	10 19	mpbi	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
21	2	oveq2i	⊢ ( ( II ×t II ) Cn II ) = ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
22	20 21	eleqtrri	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II )