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 ‘ 𝐷 ) 𝑆 ) )