This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blin

Description: The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Assertion blin ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
2 1 ad4ant124 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
3 simplrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ* )
4 simplrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ℝ* )
5 xrltmin ⊢ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) → ( ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ↔ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
6 2 3 4 5 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ↔ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
7 6 pm5.32da ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
8 ifcl ⊢ ( ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) → if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ* )
9 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
10 9 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
11 8 10 sylan2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
12 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
13 12 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
14 13 adantrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
15 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
16 15 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
17 16 adantrl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
18 14 17 anbi12d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
19 elin ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )
20 anandi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
21 18 19 20 3bitr4g ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
22 7 11 21 3bitr4rd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
23 22 eqrdv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) )