Theorem xrge0mulc1cn

Description: The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017)

	Ref	Expression
Hypotheses	xrge0mulc1cn.k	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
	xrge0mulc1cn.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ ( 𝑥 ·e 𝐶 ) )
	xrge0mulc1cn.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
Assertion	xrge0mulc1cn	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0mulc1cn.k	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
2		xrge0mulc1cn.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ ( 𝑥 ·e 𝐶 ) )
3		xrge0mulc1cn.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
4		letopon	⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
5		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6		resttopon	⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) )
7	4 5 6	mp2an	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
8	1 7	eqeltri	⊢ 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
9	8	a1i	⊢ ( 𝐶 = 0 → 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) )
10		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
11	10	a1i	⊢ ( 𝐶 = 0 → 0 ∈ ( 0 [,] +∞ ) )
12		simpl	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝐶 = 0 )
13	12	oveq2d	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 𝐶 ) = ( 𝑥 ·e 0 ) )
14		simpr	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
15	5 14	sselid	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝑥 ∈ ℝ* )
16		xmul01	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ·e 0 ) = 0 )
17	15 16	syl	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 0 ) = 0 )
18	13 17	eqtrd	⊢ ( ( 𝐶 = 0 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 𝐶 ) = 0 )
19	18	mpteq2dva	⊢ ( 𝐶 = 0 → ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ ( 𝑥 ·e 𝐶 ) ) = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ 0 ) )
20		fconstmpt	⊢ ( ( 0 [,] +∞ ) × { 0 } ) = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ 0 )
21	19 2 20	3eqtr4g	⊢ ( 𝐶 = 0 → 𝐹 = ( ( 0 [,] +∞ ) × { 0 } ) )
22		c0ex	⊢ 0 ∈ V
23	22	fconst2	⊢ ( 𝐹 : ( 0 [,] +∞ ) ⟶ { 0 } ↔ 𝐹 = ( ( 0 [,] +∞ ) × { 0 } ) )
24	21 23	sylibr	⊢ ( 𝐶 = 0 → 𝐹 : ( 0 [,] +∞ ) ⟶ { 0 } )
25		cnconst	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) ) ∧ ( 0 ∈ ( 0 [,] +∞ ) ∧ 𝐹 : ( 0 [,] +∞ ) ⟶ { 0 } ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
26	9 9 11 24 25	syl22anc	⊢ ( 𝐶 = 0 → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
28		eqid	⊢ ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ )
29		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·e 𝐶 ) = ( 𝑦 ·e 𝐶 ) )
30	29	cbvmptv	⊢ ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) = ( 𝑦 ∈ ℝ* ↦ ( 𝑦 ·e 𝐶 ) )
31		id	⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ+ )
32	28 30 31	xrmulc1cn	⊢ ( 𝐶 ∈ ℝ+ → ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ∈ ( ( ordTop ‘ ≤ ) Cn ( ordTop ‘ ≤ ) ) )
33		letopuni	⊢ ℝ* = ∪ ( ordTop ‘ ≤ )
34	33	cnrest	⊢ ( ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ∈ ( ( ordTop ‘ ≤ ) Cn ( ordTop ‘ ≤ ) ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ↾ ( 0 [,] +∞ ) ) ∈ ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) Cn ( ordTop ‘ ≤ ) ) )
35	32 5 34	sylancl	⊢ ( 𝐶 ∈ ℝ+ → ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ↾ ( 0 [,] +∞ ) ) ∈ ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) Cn ( ordTop ‘ ≤ ) ) )
36		resmpt	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ↾ ( 0 [,] +∞ ) ) = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ ( 𝑥 ·e 𝐶 ) ) )
37	5 36	ax-mp	⊢ ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ↾ ( 0 [,] +∞ ) ) = ( 𝑥 ∈ ( 0 [,] +∞ ) ↦ ( 𝑥 ·e 𝐶 ) )
38	37 2	eqtr4i	⊢ ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) ) ↾ ( 0 [,] +∞ ) ) = 𝐹
39	1	eqcomi	⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = 𝐽
40	39	oveq1i	⊢ ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) Cn ( ordTop ‘ ≤ ) ) = ( 𝐽 Cn ( ordTop ‘ ≤ ) )
41	35 38 40	3eltr3g	⊢ ( 𝐶 ∈ ℝ+ → 𝐹 ∈ ( 𝐽 Cn ( ordTop ‘ ≤ ) ) )
42	4	a1i	⊢ ( 𝐶 ∈ ℝ+ → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) )
43		simpr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
44		ioorp	⊢ ( 0 (,) +∞ ) = ℝ+
45		ioossicc	⊢ ( 0 (,) +∞ ) ⊆ ( 0 [,] +∞ )
46	44 45	eqsstrri	⊢ ℝ+ ⊆ ( 0 [,] +∞ )
47		simpl	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ℝ+ )
48	46 47	sselid	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
49		ge0xmulcl	⊢ ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 𝐶 ) ∈ ( 0 [,] +∞ ) )
50	43 48 49	syl2anc	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( 𝑥 ·e 𝐶 ) ∈ ( 0 [,] +∞ ) )
51	50 2	fmptd	⊢ ( 𝐶 ∈ ℝ+ → 𝐹 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) )
52	51	frnd	⊢ ( 𝐶 ∈ ℝ+ → ran 𝐹 ⊆ ( 0 [,] +∞ ) )
53	5	a1i	⊢ ( 𝐶 ∈ ℝ+ → ( 0 [,] +∞ ) ⊆ ℝ* )
54		cnrest2	⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ ran 𝐹 ⊆ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( 𝐹 ∈ ( 𝐽 Cn ( ordTop ‘ ≤ ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) ) )
55	42 52 53 54	syl3anc	⊢ ( 𝐶 ∈ ℝ+ → ( 𝐹 ∈ ( 𝐽 Cn ( ordTop ‘ ≤ ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) ) )
56	41 55	mpbid	⊢ ( 𝐶 ∈ ℝ+ → 𝐹 ∈ ( 𝐽 Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) )
57	1	oveq2i	⊢ ( 𝐽 Cn 𝐽 ) = ( 𝐽 Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) )
58	56 57	eleqtrrdi	⊢ ( 𝐶 ∈ ℝ+ → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
59	58 44	eleq2s	⊢ ( 𝐶 ∈ ( 0 (,) +∞ ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
60	59	adantl	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 (,) +∞ ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )
61		0xr	⊢ 0 ∈ ℝ*
62		pnfxr	⊢ +∞ ∈ ℝ*
63		0ltpnf	⊢ 0 < +∞
64		elicoelioo	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞ ) → ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 = 0 ∨ 𝐶 ∈ ( 0 (,) +∞ ) ) ) )
65	61 62 63 64	mp3an	⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 = 0 ∨ 𝐶 ∈ ( 0 (,) +∞ ) ) )
66	3 65	sylib	⊢ ( 𝜑 → ( 𝐶 = 0 ∨ 𝐶 ∈ ( 0 (,) +∞ ) ) )
67	27 60 66	mpjaodan	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )