Metamath Proof Explorer

Theorem xrge0pluscn

Description: The addition operation of the extended nonnegative real numbers monoid is continuous. (Contributed by Thierry Arnoux, 24-Mar-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 
|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
xrge0iifhmeo.k 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
xrge0pluscn.1 
|- .+ = ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
Assertion xrge0pluscn 
|- .+ e. ( ( J tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 xrge0iifhmeo.k 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3 xrge0pluscn.1 
 |-  .+ = ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
4 1 2 xrge0iifhmeo 
 |-  F e. ( II Homeo J )
5 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
6 xpss12 
 |-  ( ( ( 0 [,] 1 ) C_ CC /\ ( 0 [,] 1 ) C_ CC ) -> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( CC X. CC ) )
7 5 5 6 mp2an 
 |-  ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( CC X. CC )
8 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
9 ffn 
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
10 fnssresb 
 |-  ( x. Fn ( CC X. CC ) -> ( ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) <-> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( CC X. CC ) ) )
11 8 9 10 mp2b 
 |-  ( ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) <-> ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) C_ ( CC X. CC ) )
12 7 11 mpbir 
 |-  ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) )
13 ovres 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) = ( u x. v ) )
14 iimulcl 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( u x. v ) e. ( 0 [,] 1 ) )
15 13 14 eqeltrd 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) e. ( 0 [,] 1 ) )
16 15 rgen2 
 |-  A. u e. ( 0 [,] 1 ) A. v e. ( 0 [,] 1 ) ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) e. ( 0 [,] 1 )
17 ffnov 
 |-  ( ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 ) <-> ( ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) /\ A. u e. ( 0 [,] 1 ) A. v e. ( 0 [,] 1 ) ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) e. ( 0 [,] 1 ) ) )
18 12 16 17 mpbir2an 
 |-  ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) : ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) --> ( 0 [,] 1 )
19 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
20 xpss12 
 |-  ( ( ( 0 [,] +oo ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) C_ ( RR* X. RR* ) )
21 19 19 20 mp2an 
 |-  ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) C_ ( RR* X. RR* )
22 xaddf 
 |-  +e : ( RR* X. RR* ) --> RR*
23 ffn 
 |-  ( +e : ( RR* X. RR* ) --> RR* -> +e Fn ( RR* X. RR* ) )
24 fnssresb 
 |-  ( +e Fn ( RR* X. RR* ) -> ( ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) <-> ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) C_ ( RR* X. RR* ) ) )
25 22 23 24 mp2b 
 |-  ( ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) <-> ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) C_ ( RR* X. RR* ) )
26 21 25 mpbir 
 |-  ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) )
27 3 fneq1i 
 |-  ( .+ Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) <-> ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
28 26 27 mpbir 
 |-  .+ Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) )
29 3 oveqi 
 |-  ( a .+ b ) = ( a ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) b )
30 ovres 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> ( a ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) b ) = ( a +e b ) )
31 ge0xaddcl 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> ( a +e b ) e. ( 0 [,] +oo ) )
32 30 31 eqeltrd 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> ( a ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) b ) e. ( 0 [,] +oo ) )
33 29 32 eqeltrid 
 |-  ( ( a e. ( 0 [,] +oo ) /\ b e. ( 0 [,] +oo ) ) -> ( a .+ b ) e. ( 0 [,] +oo ) )
34 33 rgen2 
 |-  A. a e. ( 0 [,] +oo ) A. b e. ( 0 [,] +oo ) ( a .+ b ) e. ( 0 [,] +oo )
35 ffnov 
 |-  ( .+ : ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) --> ( 0 [,] +oo ) <-> ( .+ Fn ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) /\ A. a e. ( 0 [,] +oo ) A. b e. ( 0 [,] +oo ) ( a .+ b ) e. ( 0 [,] +oo ) ) )
36 28 34 35 mpbir2an 
 |-  .+ : ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) --> ( 0 [,] +oo )
37 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
38 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
39 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) )
40 38 19 39 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) )
41 2 40 eqeltri 
 |-  J e. ( TopOn ` ( 0 [,] +oo ) )
42 3 oveqi 
 |-  ( ( F ` u ) .+ ( F ` v ) ) = ( ( F ` u ) ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( F ` v ) )
43 1 xrge0iifcnv 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( y e. ( 0 [,] +oo ) |-> if ( y = +oo , 0 , ( exp ` -u y ) ) ) )
44 43 simpli 
 |-  F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )
45 f1of 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) )
46 44 45 ax-mp 
 |-  F : ( 0 [,] 1 ) --> ( 0 [,] +oo )
47 46 ffvelrni 
 |-  ( u e. ( 0 [,] 1 ) -> ( F ` u ) e. ( 0 [,] +oo ) )
48 46 ffvelrni 
 |-  ( v e. ( 0 [,] 1 ) -> ( F ` v ) e. ( 0 [,] +oo ) )
49 ovres 
 |-  ( ( ( F ` u ) e. ( 0 [,] +oo ) /\ ( F ` v ) e. ( 0 [,] +oo ) ) -> ( ( F ` u ) ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( F ` v ) ) = ( ( F ` u ) +e ( F ` v ) ) )
50 47 48 49 syl2an 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` u ) ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) ( F ` v ) ) = ( ( F ` u ) +e ( F ` v ) ) )
51 42 50 syl5eq 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( ( F ` u ) .+ ( F ` v ) ) = ( ( F ` u ) +e ( F ` v ) ) )
52 1 2 xrge0iifhom 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( F ` ( u x. v ) ) = ( ( F ` u ) +e ( F ` v ) ) )
53 13 eqcomd 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( u x. v ) = ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) )
54 53 fveq2d 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( F ` ( u x. v ) ) = ( F ` ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) ) )
55 51 52 54 3eqtr2rd 
 |-  ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) -> ( F ` ( u ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) v ) ) = ( ( F ` u ) .+ ( F ` v ) ) )
56 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) )
57 56 iistmd 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. TopMnd
58 cnfldex 
 |-  CCfld e. _V
59 ovex 
 |-  ( 0 [,] 1 ) e. _V
60 eqid 
 |-  ( CCfld |`s ( 0 [,] 1 ) ) = ( CCfld |`s ( 0 [,] 1 ) )
61 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
62 60 61 mgpress 
 |-  ( ( CCfld e. _V /\ ( 0 [,] 1 ) e. _V ) -> ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) ) )
63 58 59 62 mp2an 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) )
64 60 dfii4 
 |-  II = ( TopOpen ` ( CCfld |`s ( 0 [,] 1 ) ) )
65 63 64 mgptopn 
 |-  II = ( TopOpen ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
66 cnfldbas 
 |-  CC = ( Base ` CCfld )
67 61 66 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
68 cnfldmul 
 |-  x. = ( .r ` CCfld )
69 61 68 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
70 8 9 ax-mp 
 |-  x. Fn ( CC X. CC )
71 67 56 69 70 5 ressplusf 
 |-  ( +f ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) ) = ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
72 71 eqcomi 
 |-  ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) = ( +f ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
73 65 72 tmdcn 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. TopMnd -> ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( ( II tX II ) Cn II ) )
74 57 73 ax-mp 
 |-  ( x. |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( ( II tX II ) Cn II )
75 4 18 36 37 41 55 74 mndpluscn 
 |-  .+ e. ( ( J tX J ) Cn J )