Theorem iihalf1cn

Description: The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014)

	Ref	Expression
Hypothesis	iihalf1cn.1	⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
Assertion	iihalf1cn	⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II )

Proof

Step	Hyp	Ref	Expression
1		iihalf1cn.1	⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3		dfii2	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
4		0re	⊢ 0 ∈ ℝ
5		halfre	⊢ ( 1 / 2 ) ∈ ℝ
6		iccssre	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
7	4 5 6	mp2an	⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
8	7	a1i	⊢ ( ⊤ → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
9		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
10	9	a1i	⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ )
11		iihalf1	⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
12	11	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
13	2	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14	13	a1i	⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
15		2cnd	⊢ ( ⊤ → 2 ∈ ℂ )
16	14 14 15	cnmptc	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17	14	cnmptid	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
18	2	mulcn	⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
19	18	a1i	⊢ ( ⊤ → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
20	14 16 17 19	cnmpt12f	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
21	2 1 3 8 10 12 20	cnmptre	⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II ) )
22	21	mptru	⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II )