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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
xrge0pluscn.1 ⊢ + = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
Assertion xrge0pluscn + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2 xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3 xrge0pluscn.1 ⊢ + = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
4 1 2 xrge0iifhmeo ⊢ 𝐹 ∈ ( II Homeo 𝐽 )
5 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
6 xpss12 ⊢ ( ( ( 0 [,] 1 ) ⊆ ℂ ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ ( ℂ × ℂ ) )
7 5 5 6 mp2an ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ ( ℂ × ℂ )
8 ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
9 ffn ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
10 fnssresb ⊢ ( · Fn ( ℂ × ℂ ) → ( ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ ( ℂ × ℂ ) ) )
11 8 9 10 mp2b ⊢ ( ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⊆ ( ℂ × ℂ ) )
12 7 11 mpbir ⊢ ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) )
13 ovres ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) = ( 𝑢 · 𝑣 ) )
14 iimulcl ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 · 𝑣 ) ∈ ( 0 [,] 1 ) )
15 13 14 eqeltrd ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) ∈ ( 0 [,] 1 ) )
16 15 rgen2 ⊢ ∀ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑣 ∈ ( 0 [,] 1 ) ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) ∈ ( 0 [,] 1 )
17 ffnov ⊢ ( ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) ↔ ( ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∧ ∀ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑣 ∈ ( 0 [,] 1 ) ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) ∈ ( 0 [,] 1 ) ) )
18 12 16 17 mpbir2an ⊢ ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 )
19 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
20 xpss12 ⊢ ( ( ( 0 [,] +∞ ) ⊆ ℝ* ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⊆ ( ℝ* × ℝ* ) )
21 19 19 20 mp2an ⊢ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⊆ ( ℝ* × ℝ* )
22 xaddf ⊢ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ*
23 ffn ⊢ ( +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* → +𝑒 Fn ( ℝ* × ℝ* ) )
24 fnssresb ⊢ ( +𝑒 Fn ( ℝ* × ℝ* ) → ( ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ↔ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⊆ ( ℝ* × ℝ* ) ) )
25 22 23 24 mp2b ⊢ ( ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ↔ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⊆ ( ℝ* × ℝ* ) )
26 21 25 mpbir ⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) )
27 3 fneq1i ⊢ ( + Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ↔ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
28 26 27 mpbir ⊢ + Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) )
29 3 oveqi ⊢ ( 𝑎 + 𝑏 ) = ( 𝑎 ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) 𝑏 )
30 ovres ⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) 𝑏 ) = ( 𝑎 +𝑒 𝑏 ) )
31 ge0xaddcl ⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 +𝑒 𝑏 ) ∈ ( 0 [,] +∞ ) )
32 30 31 eqeltrd ⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) 𝑏 ) ∈ ( 0 [,] +∞ ) )
33 29 32 eqeltrid ⊢ ( ( 𝑎 ∈ ( 0 [,] +∞ ) ∧ 𝑏 ∈ ( 0 [,] +∞ ) ) → ( 𝑎 + 𝑏 ) ∈ ( 0 [,] +∞ ) )
34 33 rgen2 ⊢ ∀ 𝑎 ∈ ( 0 [,] +∞ ) ∀ 𝑏 ∈ ( 0 [,] +∞ ) ( 𝑎 + 𝑏 ) ∈ ( 0 [,] +∞ )
35 ffnov ⊢ ( + : ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⟶ ( 0 [,] +∞ ) ↔ ( + Fn ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ∧ ∀ 𝑎 ∈ ( 0 [,] +∞ ) ∀ 𝑏 ∈ ( 0 [,] +∞ ) ( 𝑎 + 𝑏 ) ∈ ( 0 [,] +∞ ) ) )
36 28 34 35 mpbir2an ⊢ + : ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ⟶ ( 0 [,] +∞ )
37 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
38 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
39 resttopon ⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) )
40 38 19 39 mp2an ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
41 2 40 eqeltri ⊢ 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
42 3 oveqi ⊢ ( ( 𝐹 ‘ 𝑢 ) + ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( 𝐹 ‘ 𝑣 ) )
43 1 xrge0iifcnv ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) )
44 43 simpli ⊢ 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ )
45 f1of ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) → 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ ) )
46 44 45 ax-mp ⊢ 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ )
47 46 ffvelrni ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑢 ) ∈ ( 0 [,] +∞ ) )
48 46 ffvelrni ⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑣 ) ∈ ( 0 [,] +∞ ) )
49 ovres ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 0 [,] +∞ ) ) → ( ( 𝐹 ‘ 𝑢 ) ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +𝑒 ( 𝐹 ‘ 𝑣 ) ) )
50 47 48 49 syl2an ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ 𝑢 ) ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +𝑒 ( 𝐹 ‘ 𝑣 ) ) )
51 42 50 syl5eq ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ 𝑢 ) + ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +𝑒 ( 𝐹 ‘ 𝑣 ) ) )
52 1 2 xrge0iifhom ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑢 · 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +𝑒 ( 𝐹 ‘ 𝑣 ) ) )
53 13 eqcomd ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 · 𝑣 ) = ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) )
54 53 fveq2d ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑢 · 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) ) )
55 51 52 54 3eqtr2rd ⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑢 ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) + ( 𝐹 ‘ 𝑣 ) ) )
56 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) )
57 56 iistmd ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd
58 cnfldex ⊢ ℂfld ∈ V
59 ovex ⊢ ( 0 [,] 1 ) ∈ V
60 eqid ⊢ ( ℂfld ↾s ( 0 [,] 1 ) ) = ( ℂfld ↾s ( 0 [,] 1 ) )
61 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
62 60 61 mgpress ⊢ ( ( ℂfld ∈ V ∧ ( 0 [,] 1 ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) )
63 58 59 62 mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) )
64 60 dfii4 ⊢ II = ( TopOpen ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) )
65 63 64 mgptopn ⊢ II = ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
66 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
67 61 66 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
68 cnfldmul ⊢ · = ( .r ‘ ℂfld )
69 61 68 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
70 8 9 ax-mp ⊢ · Fn ( ℂ × ℂ )
71 67 56 69 70 5 ressplusf ⊢ ( +𝑓 ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) = ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
72 71 eqcomi ⊢ ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) = ( +𝑓 ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
73 65 72 tmdcn ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd → ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ( II ×t II ) Cn II ) )
74 57 73 ax-mp ⊢ ( · ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ( II ×t II ) Cn II )
75 4 18 36 37 41 55 74 mndpluscn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )