Metamath Proof Explorer


Theorem xblcntrps

Description: A ball contains its center. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion xblcntrps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃𝑋 )
2 psmet0 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑃 𝐷 𝑃 ) = 0 )
3 2 3adant3 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 𝐷 𝑃 ) = 0 )
4 simp3r ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 0 < 𝑅 )
5 3 4 eqbrtrd ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 𝐷 𝑃 ) < 𝑅 )
6 elblps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃𝑋 ∧ ( 𝑃 𝐷 𝑃 ) < 𝑅 ) ) )
7 6 3adant3r ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑃𝑋 ∧ ( 𝑃 𝐷 𝑃 ) < 𝑅 ) ) )
8 1 5 7 mpbir2and ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )