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	ffvelcdmi	⊢ ( 𝑢 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑢 ) ∈ ( 0 [,] +∞ ) )
48	46	ffvelcdmi	⊢ ( 𝑣 ∈ ( 0 [,] 1 ) → ( 𝐹 ‘ 𝑣 ) ∈ ( 0 [,] +∞ ) )
49		ovres	⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝐹 ‘ 𝑣 ) ∈ ( 0 [,] +∞ ) ) → ( ( 𝐹 ‘ 𝑢 ) ( +_𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +_𝑒 ( 𝐹 ‘ 𝑣 ) ) )
50	47 48 49	syl2an	⊢ ( ( 𝑢 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ 𝑢 ) ( +_𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ( 𝐹 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) +_𝑒 ( 𝐹 ‘ 𝑣 ) ) )
51	42 50	eqtrid	⊢ ( ( 𝑢 ∈ ( 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 𝐽 )

Metamath Proof Explorer

Theorem xrge0pluscn

Proof