Metamath Proof Explorer

Theorem iihalf2cn

Description: The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 1red ⊢ ( ⊤ → 1 ∈ ℝ )
6 iccssre ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
7 4 5 6 sylancr ⊢ ( ⊤ → ( ( 1 / 2 ) [,] 1 ) ⊆ ℝ )
8 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
9 8 a1i ⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ )
10 iihalf2 ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
11 10 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
12 2 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
13 12 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
14 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
15 13 13 14 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
16 13 cnmptid ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17 2 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
18 17 a1i ⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
19 oveq12 ⊢ ( ( 𝑢 = 2 ∧ 𝑣 = 𝑥 ) → ( 𝑢 · 𝑣 ) = ( 2 · 𝑥 ) )
20 13 15 16 13 13 18 19 cnmpt12 ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
21 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
22 13 13 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 13 20 22 24 cnmpt12f ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
26 2 1 3 7 9 11 25 cnmptre ⊢ ( ⊤ → ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II ) )
27 26 mptru ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) ↦ ( ( 2 · 𝑥 ) − 1 ) ) ∈ ( 𝐽 Cn II )