Metamath Proof Explorer

Theorem iimulcn

Description: Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
6 5 a1i 
 |-  ( T. -> ( 0 [,] 1 ) C_ CC )
7 1 mpomulcn 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
8 7 a1i 
 |-  ( T. -> ( x e. CC , y e. CC |-> ( x x. y ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
9 2 4 6 2 4 6 8 cnmpt2res 
 |-  ( T. -> ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) ) )
10 9 mptru 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( TopOpen ` CCfld ) )
11 iimulcl 
 |-  ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) -> ( x x. y ) e. ( 0 [,] 1 ) )
12 11 rgen2 
 |-  A. x e. ( 0 [,] 1 ) A. y e. ( 0 [,] 1 ) ( x x. y ) e. ( 0 [,] 1 )
13 eqid 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) )
14 13 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 ) )
15 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 ) )
16 14 15 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 ) )
17 12 16 ax-mp 
 |-  ran ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) C_ ( 0 [,] 1 )
18 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 ) ) ) ) )
19 3 17 5 18 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 ) ) ) )
20 10 19 mpbi 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) )
21 2 oveq2i 
 |-  ( ( II tX II ) Cn II ) = ( ( II tX II ) Cn ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) )
22 20 21 eleqtrri 
 |-  ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( x x. y ) ) e. ( ( II tX II ) Cn II )