Metamath Proof Explorer

Theorem iihalf1cn

Description: The first 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 iihalf1cn.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2
Assertion iihalf1cn ⊢ x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ J Cn II

Proof

Step Hyp Ref Expression
1 iihalf1cn.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1 2
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
4 0red ⊢ ⊤ → 0 ∈ ℝ
5 halfre ⊢ 1 2 ∈ ℝ
6 iccssre ⊢ 0 ∈ ℝ ∧ 1 2 ∈ ℝ → 0 1 2 ⊆ ℝ
7 4 5 6 sylancl ⊢ ⊤ → 0 1 2 ⊆ ℝ
8 unitssre ⊢ 0 1 ⊆ ℝ
9 8 a1i ⊢ ⊤ → 0 1 ⊆ ℝ
10 iihalf1 ⊢ x ∈ 0 1 2 → 2 ⁢ x ∈ 0 1
11 10 adantl ⊢ ⊤ ∧ x ∈ 0 1 2 → 2 ⁢ x ∈ 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 2 1 3 7 9 11 20 cnmptre ⊢ ⊤ → x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ J Cn II
22 21 mptru ⊢ x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ J Cn II