Metamath Proof Explorer

Theorem blres

Description: A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypothesis blres.2 
|- C = ( D |` ( Y X. Y ) )
Assertion blres 
|- ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( P ( ball ` C ) R ) = ( ( P ( ball ` D ) R ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 blres.2 
 |-  C = ( D |` ( Y X. Y ) )
2 elinel2 
 |-  ( P e. ( X i^i Y ) -> P e. Y )
3 1 oveqi 
 |-  ( P C x ) = ( P ( D |` ( Y X. Y ) ) x )
4 ovres 
 |-  ( ( P e. Y /\ x e. Y ) -> ( P ( D |` ( Y X. Y ) ) x ) = ( P D x ) )
5 3 4 syl5eq 
 |-  ( ( P e. Y /\ x e. Y ) -> ( P C x ) = ( P D x ) )
6 2 5 sylan 
 |-  ( ( P e. ( X i^i Y ) /\ x e. Y ) -> ( P C x ) = ( P D x ) )
7 6 breq1d 
 |-  ( ( P e. ( X i^i Y ) /\ x e. Y ) -> ( ( P C x ) < R <-> ( P D x ) < R ) )
8 7 anbi2d 
 |-  ( ( P e. ( X i^i Y ) /\ x e. Y ) -> ( ( x e. X /\ ( P C x ) < R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
9 8 pm5.32da 
 |-  ( P e. ( X i^i Y ) -> ( ( x e. Y /\ ( x e. X /\ ( P C x ) < R ) ) <-> ( x e. Y /\ ( x e. X /\ ( P D x ) < R ) ) ) )
10 9 3ad2ant2 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( ( x e. Y /\ ( x e. X /\ ( P C x ) < R ) ) <-> ( x e. Y /\ ( x e. X /\ ( P D x ) < R ) ) ) )
11 elin 
 |-  ( x e. ( X i^i Y ) <-> ( x e. X /\ x e. Y ) )
12 11 biancomi 
 |-  ( x e. ( X i^i Y ) <-> ( x e. Y /\ x e. X ) )
13 12 anbi1i 
 |-  ( ( x e. ( X i^i Y ) /\ ( P C x ) < R ) <-> ( ( x e. Y /\ x e. X ) /\ ( P C x ) < R ) )
14 anass 
 |-  ( ( ( x e. Y /\ x e. X ) /\ ( P C x ) < R ) <-> ( x e. Y /\ ( x e. X /\ ( P C x ) < R ) ) )
15 13 14 bitri 
 |-  ( ( x e. ( X i^i Y ) /\ ( P C x ) < R ) <-> ( x e. Y /\ ( x e. X /\ ( P C x ) < R ) ) )
16 ancom 
 |-  ( ( ( x e. X /\ ( P D x ) < R ) /\ x e. Y ) <-> ( x e. Y /\ ( x e. X /\ ( P D x ) < R ) ) )
17 10 15 16 3bitr4g 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( ( x e. ( X i^i Y ) /\ ( P C x ) < R ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ x e. Y ) ) )
18 xmetres 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) )
19 1 18 eqeltrid 
 |-  ( D e. ( *Met ` X ) -> C e. ( *Met ` ( X i^i Y ) ) )
20 elbl 
 |-  ( ( C e. ( *Met ` ( X i^i Y ) ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( x e. ( P ( ball ` C ) R ) <-> ( x e. ( X i^i Y ) /\ ( P C x ) < R ) ) )
21 19 20 syl3an1 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( x e. ( P ( ball ` C ) R ) <-> ( x e. ( X i^i Y ) /\ ( P C x ) < R ) ) )
22 elin 
 |-  ( x e. ( ( P ( ball ` D ) R ) i^i Y ) <-> ( x e. ( P ( ball ` D ) R ) /\ x e. Y ) )
23 elinel1 
 |-  ( P e. ( X i^i Y ) -> P e. X )
24 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
25 23 24 syl3an2 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
26 25 anbi1d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. Y ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ x e. Y ) ) )
27 22 26 syl5bb 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( x e. ( ( P ( ball ` D ) R ) i^i Y ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ x e. Y ) ) )
28 17 21 27 3bitr4d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( x e. ( P ( ball ` C ) R ) <-> x e. ( ( P ( ball ` D ) R ) i^i Y ) ) )
29 28 eqrdv 
 |-  ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( P ( ball ` C ) R ) = ( ( P ( ball ` D ) R ) i^i Y ) )