Metamath Proof Explorer

Theorem blss2ps

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014) (Revised by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blss2ps ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2 simpl2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑃 ∈ 𝑋 )
3 simpl3 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑄 ∈ 𝑋 )
4 simpr1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ )
5 4 rexrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ* )
6 simpr2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ )
7 6 rexrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ* )
8 6 4 resubcld ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 − 𝑅 ) ∈ ℝ )
9 simpr3 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) )
10 psmetlecl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( ( 𝑆 − 𝑅 ) ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
11 1 2 3 8 9 10 syl122anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
12 rexsub ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) )
13 6 4 12 syl2anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) )
14 9 13 breqtrrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
15 1 2 3 5 7 11 14 xblss2ps ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )