Metamath Proof Explorer

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 )