Theorem circcn

Description: The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020)

	Ref	Expression
Hypotheses	circtopn.i	⊢ 𝐼 = ( 0 [,] ( 2 · π ) )
	circtopn.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	circtopn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
	circtopn.c	⊢ 𝐶 = ( ◡ abs “ { 1 } )
Assertion	circcn	⊢ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		circtopn.i	⊢ 𝐼 = ( 0 [,] ( 2 · π ) )
2		circtopn.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
3		circtopn.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
4		circtopn.c	⊢ 𝐶 = ( ◡ abs “ { 1 } )
5		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
6	2 5	eqeltri	⊢ 𝐽 ∈ ( TopOn ‘ ℝ )
7	3 4	efifo	⊢ 𝐹 : ℝ –onto→ 𝐶
8		fofn	⊢ ( 𝐹 : ℝ –onto→ 𝐶 → 𝐹 Fn ℝ )
9	7 8	ax-mp	⊢ 𝐹 Fn ℝ
10		qtopid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℝ ) ∧ 𝐹 Fn ℝ ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
11	6 9 10	mp2an	⊢ 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) )