Theorem xrmulc1cn

Description: The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017)

	Ref	Expression
Hypotheses	xrmulc1cn.k	⊢ 𝐽 = ( ordTop ‘ ≤ )
	xrmulc1cn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) )
	xrmulc1cn.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion	xrmulc1cn	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		xrmulc1cn.k	⊢ 𝐽 = ( ordTop ‘ ≤ )
2		xrmulc1cn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ* ↦ ( 𝑥 ·e 𝐶 ) )
3		xrmulc1cn.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4		letsr	⊢ ≤ ∈ TosetRel
5	4	a1i	⊢ ( 𝜑 → ≤ ∈ TosetRel )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → 𝐶 ∈ ℝ+ )
8	7	rpxrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → 𝐶 ∈ ℝ* )
9	6 8	xmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 ·e 𝐶 ) ∈ ℝ* )
10	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ* ( 𝑥 ·e 𝐶 ) ∈ ℝ* )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝐶 ∈ ℝ+ )
13	12	rpred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝐶 ∈ ℝ )
14	12	rpne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝐶 ≠ 0 )
15		xreceu	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝑦 )
16	11 13 14 15	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝑦 )
17		eqcom	⊢ ( 𝑦 = ( 𝑥 ·e 𝐶 ) ↔ ( 𝑥 ·e 𝐶 ) = 𝑦 )
18		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
19	8	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → 𝐶 ∈ ℝ* )
20		xmulcom	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ·e 𝐶 ) = ( 𝐶 ·e 𝑥 ) )
21	18 19 20	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 ·e 𝐶 ) = ( 𝐶 ·e 𝑥 ) )
22	21	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑥 ·e 𝐶 ) = 𝑦 ↔ ( 𝐶 ·e 𝑥 ) = 𝑦 ) )
23	17 22	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 = ( 𝑥 ·e 𝐶 ) ↔ ( 𝐶 ·e 𝑥 ) = 𝑦 ) )
24	23	reubidva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( ∃! 𝑥 ∈ ℝ* 𝑦 = ( 𝑥 ·e 𝐶 ) ↔ ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝑦 ) )
25	16 24	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ∃! 𝑥 ∈ ℝ* 𝑦 = ( 𝑥 ·e 𝐶 ) )
26	25	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ* ∃! 𝑥 ∈ ℝ* 𝑦 = ( 𝑥 ·e 𝐶 ) )
27	2	f1ompt	⊢ ( 𝐹 : ℝ* –1-1-onto→ ℝ* ↔ ( ∀ 𝑥 ∈ ℝ* ( 𝑥 ·e 𝐶 ) ∈ ℝ* ∧ ∀ 𝑦 ∈ ℝ* ∃! 𝑥 ∈ ℝ* 𝑦 = ( 𝑥 ·e 𝐶 ) ) )
28	10 26 27	sylanbrc	⊢ ( 𝜑 → 𝐹 : ℝ* –1-1-onto→ ℝ* )
29		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
31	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → 𝐶 ∈ ℝ+ )
32		xlemul1	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝐶 ∈ ℝ+ ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 ·e 𝐶 ) ≤ ( 𝑦 ·e 𝐶 ) ) )
33	29 30 31 32	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 ·e 𝐶 ) ≤ ( 𝑦 ·e 𝐶 ) ) )
34		ovex	⊢ ( 𝑥 ·e 𝐶 ) ∈ V
35	2	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑥 ·e 𝐶 ) ∈ V ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 ·e 𝐶 ) )
36	29 34 35	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 ·e 𝐶 ) )
37		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·e 𝐶 ) = ( 𝑦 ·e 𝐶 ) )
38		ovex	⊢ ( 𝑦 ·e 𝐶 ) ∈ V
39	37 2 38	fvmpt	⊢ ( 𝑦 ∈ ℝ* → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ·e 𝐶 ) )
40	39	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ·e 𝐶 ) )
41	36 40	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑥 ·e 𝐶 ) ≤ ( 𝑦 ·e 𝐶 ) ) )
42	33 41	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
43	42	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ* ) → ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
44	43	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
45		df-isom	⊢ ( 𝐹 Isom ≤ , ≤ ( ℝ* , ℝ* ) ↔ ( 𝐹 : ℝ* –1-1-onto→ ℝ* ∧ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
46	28 44 45	sylanbrc	⊢ ( 𝜑 → 𝐹 Isom ≤ , ≤ ( ℝ* , ℝ* ) )
47		ledm	⊢ ℝ* = dom ≤
48	47 47	ordthmeolem	⊢ ( ( ≤ ∈ TosetRel ∧ ≤ ∈ TosetRel ∧ 𝐹 Isom ≤ , ≤ ( ℝ* , ℝ* ) ) → 𝐹 ∈ ( ( ordTop ‘ ≤ ) Cn ( ordTop ‘ ≤ ) ) )
49	5 5 46 48	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ ( ( ordTop ‘ ≤ ) Cn ( ordTop ‘ ≤ ) ) )
50	1 1	oveq12i	⊢ ( 𝐽 Cn 𝐽 ) = ( ( ordTop ‘ ≤ ) Cn ( ordTop ‘ ≤ ) )
51	49 50	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐽 ) )