Theorem blsconn

Description: An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	blsconn.j	|- J = ( TopOpen ` CCfld )
	blsconn.s	|- S = ( P ( ball ` ( abs o. - ) ) R )
	blsconn.k	|- K = ( J |`t S )
Assertion	blsconn	|- ( ( P e. CC /\ R e. RR* ) -> K e. SConn )

Proof

Step	Hyp	Ref	Expression
1		blsconn.j	|- J = ( TopOpen ` CCfld )
2		blsconn.s	|- S = ( P ( ball ` ( abs o. - ) ) R )
3		blsconn.k	|- K = ( J |`t S )
4		cnxmet	|- ( abs o. - ) e. ( *Met ` CC )
5		blssm	|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ P e. CC /\ R e. RR* ) -> ( P ( ball ` ( abs o. - ) ) R ) C_ CC )
6	4 5	mp3an1	|- ( ( P e. CC /\ R e. RR* ) -> ( P ( ball ` ( abs o. - ) ) R ) C_ CC )
7	2 6	eqsstrid	|- ( ( P e. CC /\ R e. RR* ) -> S C_ CC )
8	2	blcvx	|- ( ( ( P e. CC /\ R e. RR* ) /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
9	7 8 1 3	cvxsconn	|- ( ( P e. CC /\ R e. RR* ) -> K e. SConn )