Metamath Proof Explorer


Theorem iihalf2cn

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

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

Proof

Step Hyp Ref Expression
1 iihalf2cn.1 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
2 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 dfii2 II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
4 halfre ( 1 / 2 ) ∈ ℝ
5 1re 1 ∈ ℝ
6 iccssre ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
7 4 5 6 mp2an ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ
8 7 a1i ( ⊤ → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
9 unitssre ( 0 [,] 1 ) ⊆ ℝ
10 9 a1i ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ )
11 iihalf2 ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
12 11 adantl ( ( ⊤ ∧ 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 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 1cnd ( ⊤ → 1 ∈ ℂ )
22 14 14 21 cnmptc ( ⊤ → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
23 2 subcn − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
24 23 a1i ( ⊤ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
25 14 20 22 24 cnmpt12f ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
26 2 1 3 8 10 12 25 cnmptre ( ⊤ → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II ) )
27 26 mptru ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II )