Metamath Proof Explorer

Theorem iimulcn

Description: Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014)

Ref Expression
Assertion iimulcn 
|- ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn II )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 dfii3 
 |-  II = ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) )
3 1 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
4 3 a1i 
 |-  ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
5 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
6 ax-resscn 
 |-  RR C_ CC
7 5 6 sstri 
 |-  ( 0 [,] 1 ) C_ CC
8 7 a1i 
 |-  ( T. -> ( 0 [,] 1 ) C_ CC )
9 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
10 ffn 
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
11 9 10 ax-mp 
 |-  x. Fn ( CC X. CC )
12 fnov 
 |-  ( x. Fn ( CC X. CC ) <-> x. = ( x e. CC , y e. CC |-> ( x x. y ) ) )
13 11 12 mpbi 
 |-  x. = ( x e. CC , y e. CC |-> ( x x. y ) )
14 1 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
15 13 14 eqeltrri 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
16 15 a1i 
 |-  ( T. -> ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
17 2 4 8 2 4 8 16 cnmpt2res 
 |-  ( T. -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
18 17 mptru 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) )
19 iimulcl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( x x. y ) e. ( 0 [,] 1 ) )
20 19 rgen2 
 |-  A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 )
21 eqid 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) )
22 21 fmpo 
 |-  ( A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 ) )
23 frn 
 |-  ( ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 ) -> ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) C_ ( 0 [,] 1 ) )
24 22 23 sylbi 
 |-  ( A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 ) -> ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) C_ ( 0 [,] 1 ) )
25 20 24 ax-mp 
 |-  ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) C_ ( 0 [,] 1 )
26 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ CC ) -> ( ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) ) )
27 3 25 7 26 mp3an 
 |-  ( ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) <-> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) ) )
28 18 27 mpbi 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) )
29 2 oveq2i 
 |-  ( ( II tX II ) Cn II ) = ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) )
30 28 29 eleqtrri 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn II )