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 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
Assertion iihalf2cn ⊢ x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II

Proof

Step Hyp Ref Expression
1 iihalf2cn.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 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 ⊢ x ∈ 1 2 1 → 2 ⁢ x − 1 ∈ 0 1
11 10 adantl ⊢ ⊤ ∧ x ∈ 1 2 1 → 2 ⁢ x − 1 ∈ 0 1
12 2 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
13 12 a1i ⊢ ⊤ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
14 2cnd ⊢ ⊤ → 2 ∈ ℂ
15 13 13 14 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 2 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
16 13 cnmptid ⊢ ⊤ → x ∈ ℂ ⟼ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 2 mpomulcn ⊢ u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
18 17 a1i ⊢ ⊤ → u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
19 oveq12 ⊢ u = 2 ∧ v = x → u ⁢ v = 2 ⁢ x
20 13 15 16 13 13 18 19 cnmpt12 ⊢ ⊤ → x ∈ ℂ ⟼ 2 ⁢ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
21 1cnd ⊢ ⊤ → 1 ∈ ℂ
22 13 13 21 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 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 ⊢ ⊤ → x ∈ ℂ ⟼ 2 ⁢ x − 1 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
26 2 1 3 7 9 11 25 cnmptre ⊢ ⊤ → x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II
27 26 mptru ⊢ x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II