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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	blsconn.s	⊢ 𝑆 = ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
	blsconn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
Assertion	blsconn	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → 𝐾 ∈ SConn )

Proof

Step	Hyp	Ref	Expression
1		blsconn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		blsconn.s	⊢ 𝑆 = ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
3		blsconn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
4		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
5		blssm	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
6	4 5	mp3an1	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ ℂ )
7	2 6	eqsstrid	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → 𝑆 ⊆ ℂ )
8	2	blcvx	⊢ ( ( ( 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
9	7 8 1 3	cvxsconn	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → 𝐾 ∈ SConn )