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 (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
Assertion iihalf2cn 
|- ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( J Cn II )

Proof

Step Hyp Ref Expression
1 iihalf2cn.1 
 |-  J = ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
4 halfre 
 |-  ( 1 / 2 ) e. RR
5 1red 
 |-  ( T. -> 1 e. RR )
6 iccssre 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
7 4 5 6 sylancr 
 |-  ( T. -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
8 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
9 8 a1i 
 |-  ( T. -> ( 0 [,] 1 ) C_ RR )
10 iihalf2 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
11 10 adantl 
 |-  ( ( T. /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( 2 x. x ) - 1 ) e. ( 0 [,] 1 ) )
12 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
13 12 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
14 2cnd 
 |-  ( T. -> 2 e. CC )
15 13 13 14 cnmptc 
 |-  ( T. -> ( x e. CC |-> 2 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
16 13 cnmptid 
 |-  ( T. -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
17 2 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
18 17 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
19 oveq12 
 |-  ( ( u = 2 /\ v = x ) -> ( u x. v ) = ( 2 x. x ) )
20 13 15 16 13 13 18 19 cnmpt12 
 |-  ( T. -> ( x e. CC |-> ( 2 x. x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
21 1cnd 
 |-  ( T. -> 1 e. CC )
22 13 13 21 cnmptc 
 |-  ( T. -> ( x e. CC |-> 1 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
23 2 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
24 23 a1i 
 |-  ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
25 13 20 22 24 cnmpt12f 
 |-  ( T. -> ( x e. CC |-> ( ( 2 x. x ) - 1 ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
26 2 1 3 7 9 11 25 cnmptre 
 |-  ( T. -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( J Cn II ) )
27 26 mptru 
 |-  ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( 2 x. x ) - 1 ) ) e. ( J Cn II )