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

Proof

Step Hyp Ref Expression
1 iihalf1cn.1 
 |-  J = ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
4 0re 
 |-  0 e. RR
5 halfre 
 |-  ( 1 / 2 ) e. RR
6 iccssre 
 |-  ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
7 4 5 6 mp2an 
 |-  ( 0 [,] ( 1 / 2 ) ) C_ RR
8 7 a1i 
 |-  ( T. -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
9 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
10 9 a1i 
 |-  ( T. -> ( 0 [,] 1 ) C_ RR )
11 iihalf1 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
12 11 adantl 
 |-  ( ( T. /\ x e. ( 0 [,] ( 1 / 2 ) ) ) -> ( 2 x. x ) e. ( 0 [,] 1 ) )
13 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14 13 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
15 2cnd 
 |-  ( T. -> 2 e. CC )
16 14 14 15 cnmptc 
 |-  ( T. -> ( x e. CC |-> 2 ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
17 14 cnmptid 
 |-  ( T. -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
18 2 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
19 18 a1i 
 |-  ( T. -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
20 14 16 17 19 cnmpt12f 
 |-  ( T. -> ( x e. CC |-> ( 2 x. x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
21 2 1 3 8 10 12 20 cnmptre 
 |-  ( T. -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( J Cn II ) )
22 21 mptru 
 |-  ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( J Cn II )