Metamath Proof Explorer

Theorem imasf1obl

Description: The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses imasf1obl.u 
|- ( ph -> U = ( F "s R ) )
imasf1obl.v 
|- ( ph -> V = ( Base ` R ) )
imasf1obl.f 
|- ( ph -> F : V -1-1-onto-> B )
imasf1obl.r 
|- ( ph -> R e. Z )
imasf1obl.e 
|- E = ( ( dist ` R ) |` ( V X. V ) )
imasf1obl.d 
|- D = ( dist ` U )
imasf1obl.m 
|- ( ph -> E e. ( *Met ` V ) )
imasf1obl.x 
|- ( ph -> P e. V )
imasf1obl.s 
|- ( ph -> S e. RR* )
Assertion imasf1obl 
|- ( ph -> ( ( F ` P ) ( ball ` D ) S ) = ( F " ( P ( ball ` E ) S ) ) )

Proof

Step Hyp Ref Expression
1 imasf1obl.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasf1obl.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasf1obl.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasf1obl.r 
 |-  ( ph -> R e. Z )
5 imasf1obl.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
6 imasf1obl.d 
 |-  D = ( dist ` U )
7 imasf1obl.m 
 |-  ( ph -> E e. ( *Met ` V ) )
8 imasf1obl.x 
 |-  ( ph -> P e. V )
9 imasf1obl.s 
 |-  ( ph -> S e. RR* )
10 f1ocnvfv2 
 |-  ( ( F : V -1-1-onto-> B /\ x e. B ) -> ( F ` ( `' F ` x ) ) = x )
11 3 10 sylan 
 |-  ( ( ph /\ x e. B ) -> ( F ` ( `' F ` x ) ) = x )
12 11 oveq2d 
 |-  ( ( ph /\ x e. B ) -> ( ( F ` P ) D ( F ` ( `' F ` x ) ) ) = ( ( F ` P ) D x ) )
13 1 adantr 
 |-  ( ( ph /\ x e. B ) -> U = ( F "s R ) )
14 2 adantr 
 |-  ( ( ph /\ x e. B ) -> V = ( Base ` R ) )
15 3 adantr 
 |-  ( ( ph /\ x e. B ) -> F : V -1-1-onto-> B )
16 4 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Z )
17 7 adantr 
 |-  ( ( ph /\ x e. B ) -> E e. ( *Met ` V ) )
18 8 adantr 
 |-  ( ( ph /\ x e. B ) -> P e. V )
19 f1ocnv 
 |-  ( F : V -1-1-onto-> B -> `' F : B -1-1-onto-> V )
20 3 19 syl 
 |-  ( ph -> `' F : B -1-1-onto-> V )
21 f1of 
 |-  ( `' F : B -1-1-onto-> V -> `' F : B --> V )
22 20 21 syl 
 |-  ( ph -> `' F : B --> V )
23 22 ffvelcdmda 
 |-  ( ( ph /\ x e. B ) -> ( `' F ` x ) e. V )
24 13 14 15 16 5 6 17 18 23 imasdsf1o 
 |-  ( ( ph /\ x e. B ) -> ( ( F ` P ) D ( F ` ( `' F ` x ) ) ) = ( P E ( `' F ` x ) ) )
25 12 24 eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( ( F ` P ) D x ) = ( P E ( `' F ` x ) ) )
26 25 breq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( F ` P ) D x ) < S <-> ( P E ( `' F ` x ) ) < S ) )
27 9 adantr 
 |-  ( ( ph /\ x e. B ) -> S e. RR* )
28 elbl2 
 |-  ( ( ( E e. ( *Met ` V ) /\ S e. RR* ) /\ ( P e. V /\ ( `' F ` x ) e. V ) ) -> ( ( `' F ` x ) e. ( P ( ball ` E ) S ) <-> ( P E ( `' F ` x ) ) < S ) )
29 17 27 18 23 28 syl22anc 
 |-  ( ( ph /\ x e. B ) -> ( ( `' F ` x ) e. ( P ( ball ` E ) S ) <-> ( P E ( `' F ` x ) ) < S ) )
30 26 29 bitr4d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( F ` P ) D x ) < S <-> ( `' F ` x ) e. ( P ( ball ` E ) S ) ) )
31 30 pm5.32da 
 |-  ( ph -> ( ( x e. B /\ ( ( F ` P ) D x ) < S ) <-> ( x e. B /\ ( `' F ` x ) e. ( P ( ball ` E ) S ) ) ) )
32 1 2 3 4 5 6 7 imasf1oxmet 
 |-  ( ph -> D e. ( *Met ` B ) )
33 f1of 
 |-  ( F : V -1-1-onto-> B -> F : V --> B )
34 3 33 syl 
 |-  ( ph -> F : V --> B )
35 34 8 ffvelcdmd 
 |-  ( ph -> ( F ` P ) e. B )
36 elbl 
 |-  ( ( D e. ( *Met ` B ) /\ ( F ` P ) e. B /\ S e. RR* ) -> ( x e. ( ( F ` P ) ( ball ` D ) S ) <-> ( x e. B /\ ( ( F ` P ) D x ) < S ) ) )
37 32 35 9 36 syl3anc 
 |-  ( ph -> ( x e. ( ( F ` P ) ( ball ` D ) S ) <-> ( x e. B /\ ( ( F ` P ) D x ) < S ) ) )
38 f1ofn 
 |-  ( `' F : B -1-1-onto-> V -> `' F Fn B )
39 elpreima 
 |-  ( `' F Fn B -> ( x e. ( `' `' F " ( P ( ball ` E ) S ) ) <-> ( x e. B /\ ( `' F ` x ) e. ( P ( ball ` E ) S ) ) ) )
40 20 38 39 3syl 
 |-  ( ph -> ( x e. ( `' `' F " ( P ( ball ` E ) S ) ) <-> ( x e. B /\ ( `' F ` x ) e. ( P ( ball ` E ) S ) ) ) )
41 31 37 40 3bitr4d 
 |-  ( ph -> ( x e. ( ( F ` P ) ( ball ` D ) S ) <-> x e. ( `' `' F " ( P ( ball ` E ) S ) ) ) )
42 41 eqrdv 
 |-  ( ph -> ( ( F ` P ) ( ball ` D ) S ) = ( `' `' F " ( P ( ball ` E ) S ) ) )
43 imacnvcnv 
 |-  ( `' `' F " ( P ( ball ` E ) S ) ) = ( F " ( P ( ball ` E ) S ) )
44 42 43 eqtrdi 
 |-  ( ph -> ( ( F ` P ) ( ball ` D ) S ) = ( F " ( P ( ball ` E ) S ) ) )