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 ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
xrge0iifhmeo.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
xrge0pluscn.1 ⊢ + ˙ = + 𝑒 ↾ 0 +∞ × 0 +∞
Assertion xrge0pluscn ⊢ + ˙ ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ F = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
2 xrge0iifhmeo.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
3 xrge0pluscn.1 ⊢ + ˙ = + 𝑒 ↾ 0 +∞ × 0 +∞
4 1 2 xrge0iifhmeo ⊢ F ∈ II Homeo J
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 ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → u × ↾ 0 1 × 0 1 v = u ⁢ v
14 iimulcl ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → u ⁢ v ∈ 0 1
15 13 14 eqeltrd ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → u × ↾ 0 1 × 0 1 v ∈ 0 1
16 15 rgen2 ⊢ ∀ u ∈ 0 1 ∀ v ∈ 0 1 u × ↾ 0 1 × 0 1 v ∈ 0 1
17 ffnov ⊢ × ↾ 0 1 × 0 1 : 0 1 × 0 1 ⟶ 0 1 ↔ × ↾ 0 1 × 0 1 Fn 0 1 × 0 1 ∧ ∀ u ∈ 0 1 ∀ v ∈ 0 1 u × ↾ 0 1 × 0 1 v ∈ 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 ⊢ a + ˙ b = a + 𝑒 ↾ 0 +∞ × 0 +∞ b
30 ovres ⊢ a ∈ 0 +∞ ∧ b ∈ 0 +∞ → a + 𝑒 ↾ 0 +∞ × 0 +∞ b = a + 𝑒 b
31 ge0xaddcl ⊢ a ∈ 0 +∞ ∧ b ∈ 0 +∞ → a + 𝑒 b ∈ 0 +∞
32 30 31 eqeltrd ⊢ a ∈ 0 +∞ ∧ b ∈ 0 +∞ → a + 𝑒 ↾ 0 +∞ × 0 +∞ b ∈ 0 +∞
33 29 32 eqeltrid ⊢ a ∈ 0 +∞ ∧ b ∈ 0 +∞ → a + ˙ b ∈ 0 +∞
34 33 rgen2 ⊢ ∀ a ∈ 0 +∞ ∀ b ∈ 0 +∞ a + ˙ b ∈ 0 +∞
35 ffnov ⊢ + ˙ : 0 +∞ × 0 +∞ ⟶ 0 +∞ ↔ + ˙ Fn 0 +∞ × 0 +∞ ∧ ∀ a ∈ 0 +∞ ∀ b ∈ 0 +∞ a + ˙ b ∈ 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 ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
40 38 19 39 mp2an ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
41 2 40 eqeltri ⊢ J ∈ TopOn ⁡ 0 +∞
42 3 oveqi ⊢ F ⁡ u + ˙ F ⁡ v = F ⁡ u + 𝑒 ↾ 0 +∞ × 0 +∞ F ⁡ v
43 1 xrge0iifcnv ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ if y = +∞ 0 e − y
44 43 simpli ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞
45 f1of ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ → F : 0 1 ⟶ 0 +∞
46 44 45 ax-mp ⊢ F : 0 1 ⟶ 0 +∞
47 46 ffvelrni ⊢ u ∈ 0 1 → F ⁡ u ∈ 0 +∞
48 46 ffvelrni ⊢ v ∈ 0 1 → F ⁡ v ∈ 0 +∞
49 ovres ⊢ F ⁡ u ∈ 0 +∞ ∧ F ⁡ v ∈ 0 +∞ → F ⁡ u + 𝑒 ↾ 0 +∞ × 0 +∞ F ⁡ v = F ⁡ u + 𝑒 F ⁡ v
50 47 48 49 syl2an ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → F ⁡ u + 𝑒 ↾ 0 +∞ × 0 +∞ F ⁡ v = F ⁡ u + 𝑒 F ⁡ v
51 42 50 syl5eq ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → F ⁡ u + ˙ F ⁡ v = F ⁡ u + 𝑒 F ⁡ v
52 1 2 xrge0iifhom ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → F ⁡ u ⁢ v = F ⁡ u + 𝑒 F ⁡ v
53 13 eqcomd ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → u ⁢ v = u × ↾ 0 1 × 0 1 v
54 53 fveq2d ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → F ⁡ u ⁢ v = F ⁡ u × ↾ 0 1 × 0 1 v
55 51 52 54 3eqtr2rd ⊢ u ∈ 0 1 ∧ v ∈ 0 1 → F ⁡ u × ↾ 0 1 × 0 1 v = F ⁡ u + ˙ F ⁡ v
56 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
57 56 iistmd ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 ∈ TopMnd
58 cnfldex ⊢ ℂ fld ∈ V
59 ovex ⊢ 0 1 ∈ V
60 eqid ⊢ ℂ fld ↾ 𝑠 0 1 = ℂ fld ↾ 𝑠 0 1
61 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
62 60 61 mgpress ⊢ ℂ fld ∈ V ∧ 0 1 ∈ V → mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
63 58 59 62 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
64 60 dfii4 ⊢ II = TopOpen ⁡ ℂ fld ↾ 𝑠 0 1
65 63 64 mgptopn ⊢ II = TopOpen ⁡ mulGrp ℂ fld ↾ 𝑠 0 1
66 cnfldbas ⊢ ℂ = Base ℂ fld
67 61 66 mgpbas ⊢ ℂ = Base mulGrp ℂ fld
68 cnfldmul ⊢ × = ⋅ ℂ fld
69 61 68 mgpplusg ⊢ × = + mulGrp ℂ fld
70 8 9 ax-mp ⊢ × Fn ℂ × ℂ
71 67 56 69 70 5 ressplusf ⊢ + 𝑓 ⁡ mulGrp ℂ fld ↾ 𝑠 0 1 = × ↾ 0 1 × 0 1
72 71 eqcomi ⊢ × ↾ 0 1 × 0 1 = + 𝑓 ⁡ mulGrp ℂ fld ↾ 𝑠 0 1
73 65 72 tmdcn ⊢ mulGrp ℂ fld ↾ 𝑠 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 ⊢ + ˙ ∈ J × t J Cn J