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	|- I = ( 0 [,] ( 2 x. _pi ) )
	circtopn.j	|- J = ( topGen ` ran (,) )
	circtopn.f	|- F = ( x e. RR |-> ( exp ` ( _i x. x ) ) )
	circtopn.c	|- C = ( `' abs " { 1 } )
Assertion	circcn	|- F e. ( J Cn ( J qTop F ) )

Proof

Step	Hyp	Ref	Expression
1		circtopn.i	|- I = ( 0 [,] ( 2 x. _pi ) )
2		circtopn.j	|- J = ( topGen ` ran (,) )
3		circtopn.f	|- F = ( x e. RR |-> ( exp ` ( _i x. x ) ) )
4		circtopn.c	|- C = ( `' abs " { 1 } )
5		retopon	|- ( topGen ` ran (,) ) e. ( TopOn ` RR )
6	2 5	eqeltri	|- J e. ( TopOn ` RR )
7	3 4	efifo	|- F : RR -onto-> C
8		fofn	|- ( F : RR -onto-> C -> F Fn RR )
9	7 8	ax-mp	|- F Fn RR
10		qtopid	|- ( ( J e. ( TopOn ` RR ) /\ F Fn RR ) -> F e. ( J Cn ( J qTop F ) ) )
11	6 9 10	mp2an	|- F e. ( J Cn ( J qTop F ) )