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 
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) = ( P ( ball ` D ) if ( R <_ S , R , S ) ) )

Proof

Step Hyp Ref Expression
1 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* )
2 1 ad4ant124 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) /\ x e. X ) -> ( P D x ) e. RR* )
3 simplrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) /\ x e. X ) -> R e. RR* )
4 simplrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) /\ x e. X ) -> S e. RR* )
5 xrltmin 
 |-  ( ( ( P D x ) e. RR* /\ R e. RR* /\ S e. RR* ) -> ( ( P D x ) < if ( R <_ S , R , S ) <-> ( ( P D x ) < R /\ ( P D x ) < S ) ) )
6 2 3 4 5 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) /\ x e. X ) -> ( ( P D x ) < if ( R <_ S , R , S ) <-> ( ( P D x ) < R /\ ( P D x ) < S ) ) )
7 6 pm5.32da 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( x e. X /\ ( P D x ) < if ( R <_ S , R , S ) ) <-> ( x e. X /\ ( ( P D x ) < R /\ ( P D x ) < S ) ) ) )
8 ifcl 
 |-  ( ( R e. RR* /\ S e. RR* ) -> if ( R <_ S , R , S ) e. RR* )
9 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ if ( R <_ S , R , S ) e. RR* ) -> ( x e. ( P ( ball ` D ) if ( R <_ S , R , S ) ) <-> ( x e. X /\ ( P D x ) < if ( R <_ S , R , S ) ) ) )
10 9 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ if ( R <_ S , R , S ) e. RR* ) -> ( x e. ( P ( ball ` D ) if ( R <_ S , R , S ) ) <-> ( x e. X /\ ( P D x ) < if ( R <_ S , R , S ) ) ) )
11 8 10 sylan2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( x e. ( P ( ball ` D ) if ( R <_ S , R , S ) ) <-> ( x e. X /\ ( P D x ) < if ( R <_ S , R , S ) ) ) )
12 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
13 12 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
14 13 adantrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
15 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( x e. ( P ( ball ` D ) S ) <-> ( x e. X /\ ( P D x ) < S ) ) )
16 15 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ S e. RR* ) -> ( x e. ( P ( ball ` D ) S ) <-> ( x e. X /\ ( P D x ) < S ) ) )
17 16 adantrl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( x e. ( P ( ball ` D ) S ) <-> ( x e. X /\ ( P D x ) < S ) ) )
18 14 17 anbi12d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( P ( ball ` D ) S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( P D x ) < S ) ) ) )
19 elin 
 |-  ( x e. ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) <-> ( x e. ( P ( ball ` D ) R ) /\ x e. ( P ( ball ` D ) S ) ) )
20 anandi 
 |-  ( ( x e. X /\ ( ( P D x ) < R /\ ( P D x ) < S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( P D x ) < S ) ) )
21 18 19 20 3bitr4g 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( x e. ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) <-> ( x e. X /\ ( ( P D x ) < R /\ ( P D x ) < S ) ) ) )
22 7 11 21 3bitr4rd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( x e. ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) <-> x e. ( P ( ball ` D ) if ( R <_ S , R , S ) ) ) )
23 22 eqrdv 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) = ( P ( ball ` D ) if ( R <_ S , R , S ) ) )