Metamath Proof Explorer


Theorem bldisj

Description: Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013)

Ref Expression
Assertion bldisj ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 simpr3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) )
2 simpr1 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑅 ∈ ℝ* )
3 simpr2 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑆 ∈ ℝ* )
4 2 3 xaddcld ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* )
5 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
6 5 adantr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
7 4 6 xrlenltd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
8 1 7 mpbid ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) )
9 elin ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
10 simpl1 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 simpl2 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑃𝑋 )
12 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
13 10 11 2 12 syl3anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
14 simpl3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑄𝑋 )
15 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄𝑋𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
16 10 14 3 15 syl3anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
17 13 16 anbi12d ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
18 anandi ( ( 𝑥𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ↔ ( ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
19 17 18 bitr4di ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
20 10 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
21 11 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝑃𝑋 )
22 simpr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
23 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
24 20 21 22 23 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
25 14 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝑄𝑋 )
26 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄𝑋𝑥𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
27 20 25 22 26 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
28 2 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝑅 ∈ ℝ* )
29 3 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → 𝑆 ∈ ℝ* )
30 xlt2add ( ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ ( 𝑄 𝐷 𝑥 ) ∈ ℝ* ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ) ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) )
31 24 27 28 29 30 syl22anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) )
32 xmettri3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃𝑋𝑄𝑋𝑥𝑋 ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) )
33 20 21 25 22 32 syl13anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) )
34 6 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
35 24 27 xaddcld ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ* )
36 4 adantr ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* )
37 xrlelttr ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ* ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
38 34 35 36 37 syl3anc ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
39 33 38 mpand ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
40 31 39 syld ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
41 40 expimpd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
42 19 41 sylbid ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
43 9 42 syl5bi ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
44 8 43 mtod ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
45 44 eq0rdv ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑄𝑋 ) ∧ ( 𝑅 ∈ ℝ*𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )