Metamath Proof Explorer

Theorem iihalf1cn

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

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 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 ⊢ x ∈ 0 1 2 → 2 ⁢ x ∈ 0 1
12 11 adantl ⊢ ⊤ ∧ x ∈ 0 1 2 → 2 ⁢ x ∈ 0 1
13 2 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
14 13 a1i ⊢ ⊤ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
15 2cnd ⊢ ⊤ → 2 ∈ ℂ
16 14 14 15 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 2 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 14 cnmptid ⊢ ⊤ → x ∈ ℂ ⟼ x ∈ 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 ⊢ ⊤ → x ∈ ℂ ⟼ 2 ⁢ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
21 2 1 3 8 10 12 20 cnmptre ⊢ ⊤ → x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ J Cn II
22 21 mptru ⊢ x ∈ 0 1 2 ⟼ 2 ⁢ x ∈ J Cn II