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

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
2 xrge0iifhmeo.k ⊢J=ordTop⁡≤↾𝑡0+∞
3 xrge0pluscn.1 ⊢+˙=+𝑒↾0+∞×0+∞
4 1 2 xrge0iifhmeo ⊢F∈IIHomeoJ
5 unitsscn ⊢01⊆ℂ
6 xpss12 ⊢01⊆ℂ∧01⊆ℂ→01×01⊆ℂ×ℂ
7 5 5 6 mp2an ⊢01×01⊆ℂ×ℂ
8 ax-mulf ⊢×:ℂ×ℂ⟶ℂ
9 ffn ⊢×:ℂ×ℂ⟶ℂ→×Fnℂ×ℂ
10 fnssresb ⊢×Fnℂ×ℂ→×↾01×01Fn01×01↔01×01⊆ℂ×ℂ
11 8 9 10 mp2b ⊢×↾01×01Fn01×01↔01×01⊆ℂ×ℂ
12 7 11 mpbir ⊢×↾01×01Fn01×01
13 ovres ⊢u∈01∧v∈01→u×↾01×01v=u⁢v
14 iimulcl ⊢u∈01∧v∈01→u⁢v∈01
15 13 14 eqeltrd ⊢u∈01∧v∈01→u×↾01×01v∈01
16 15 rgen2 ⊢∀u∈01∀v∈01u×↾01×01v∈01
17 ffnov ⊢×↾01×01:01×01⟶01↔×↾01×01Fn01×01∧∀u∈01∀v∈01u×↾01×01v∈01
18 12 16 17 mpbir2an ⊢×↾01×01:01×01⟶01
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+∞Fn0+∞×0+∞↔0+∞×0+∞⊆ℝ*×ℝ*
25 22 23 24 mp2b ⊢+𝑒↾0+∞×0+∞Fn0+∞×0+∞↔0+∞×0+∞⊆ℝ*×ℝ*
26 21 25 mpbir ⊢+𝑒↾0+∞×0+∞Fn0+∞×0+∞
27 3 fneq1i ⊢+˙Fn0+∞×0+∞↔+𝑒↾0+∞×0+∞Fn0+∞×0+∞
28 26 27 mpbir ⊢+˙Fn0+∞×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+∞↔+˙Fn0+∞×0+∞∧∀a∈0+∞∀b∈0+∞a+˙b∈0+∞
36 28 34 35 mpbir2an ⊢+˙:0+∞×0+∞⟶0+∞
37 iitopon ⊢II∈TopOn⁡01
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:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞0e−y
44 43 simpli ⊢F:01⟶1-1 onto0+∞
45 f1of ⊢F:01⟶1-1 onto0+∞→F:01⟶0+∞
46 44 45 ax-mp ⊢F:01⟶0+∞
47 46 ffvelcdmi ⊢u∈01→F⁡u∈0+∞
48 46 ffvelcdmi ⊢v∈01→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∈01∧v∈01→F⁡u+𝑒↾0+∞×0+∞F⁡v=F⁡u+𝑒F⁡v
51 42 50 eqtrid ⊢u∈01∧v∈01→F⁡u+˙F⁡v=F⁡u+𝑒F⁡v
52 1 2 xrge0iifhom ⊢u∈01∧v∈01→F⁡u⁢v=F⁡u+𝑒F⁡v
53 13 eqcomd ⊢u∈01∧v∈01→u⁢v=u×↾01×01v
54 53 fveq2d ⊢u∈01∧v∈01→F⁡u⁢v=F⁡u×↾01×01v
55 51 52 54 3eqtr2rd ⊢u∈01∧v∈01→F⁡u×↾01×01v=F⁡u+˙F⁡v
56 eqid ⊢mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
57 56 iistmd ⊢mulGrpℂfld↾𝑠01∈TopMnd
58 cnfldex ⊢ℂfld∈V
59 ovex ⊢01∈V
60 eqid ⊢ℂfld↾𝑠01=ℂfld↾𝑠01
61 eqid ⊢mulGrpℂfld=mulGrpℂfld
62 60 61 mgpress ⊢ℂfld∈V∧01∈V→mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
63 58 59 62 mp2an ⊢mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
64 60 dfii4 ⊢II=TopOpen⁡ℂfld↾𝑠01
65 63 64 mgptopn ⊢II=TopOpen⁡mulGrpℂfld↾𝑠01
66 cnfldbas ⊢ℂ=Baseℂfld
67 61 66 mgpbas ⊢ℂ=BasemulGrpℂ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↾𝑠01=×↾01×01
72 71 eqcomi ⊢×↾01×01=+𝑓⁡mulGrpℂfld↾𝑠01
73 65 72 tmdcn ⊢mulGrpℂfld↾𝑠01∈TopMnd→×↾01×01∈II×tIICnII
74 57 73 ax-mp ⊢×↾01×01∈II×tIICnII
75 4 18 36 37 41 55 74 mndpluscn ⊢+˙∈J×tJCnJ