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=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	blsconn.s	$$⊢S=P\mathrm{ball}\left(\mathrm{abs}\circ -\right)R$$
	blsconn.k	$$⊢K=J{\upharpoonright }_{𝑡}S$$
Assertion	blsconn	$$⊢\left(P\in ℂ\wedge R\in {ℝ}^{*}\right)\to K\in \mathrm{SConn}$$

Proof

Step	Hyp	Ref	Expression
1		blsconn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		blsconn.s	$$⊢S=P\mathrm{ball}\left(\mathrm{abs}\circ -\right)R$$
3		blsconn.k	$$⊢K=J{\upharpoonright }_{𝑡}S$$
4		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
5		blssm	$$⊢\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge P\in ℂ\wedge R\in {ℝ}^{*}\right)\to P\mathrm{ball}\left(\mathrm{abs}\circ -\right)R\subseteq ℂ$$
6	4 5	mp3an1	$$⊢\left(P\in ℂ\wedge R\in {ℝ}^{*}\right)\to P\mathrm{ball}\left(\mathrm{abs}\circ -\right)R\subseteq ℂ$$
7	2 6	eqsstrid	$$⊢\left(P\in ℂ\wedge R\in {ℝ}^{*}\right)\to S\subseteq ℂ$$
8	2	blcvx	$$⊢\left(\left(P\in ℂ\wedge R\in {ℝ}^{*}\right)\wedge \left(x\in S\wedge y\in S\wedge t\in \left[0,1\right]\right)\right)\to tx+\left(1-t\right)y\in S$$
9	7 8 1 3	cvxsconn	$$⊢\left(P\in ℂ\wedge R\in {ℝ}^{*}\right)\to K\in \mathrm{SConn}$$