Metamath Proof Explorer

Theorem ismtyima

Description: The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014)

Ref Expression
Assertion ismtyima 
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F " ( P ( ball ` M ) R ) ) = ( ( F ` P ) ( ball ` N ) R ) )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( F " ( P ( ball ` M ) R ) ) C_ ran F
2 isismty 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )
3 2 biimp3a 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
4 3 adantr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
5 4 simpld 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> F : X -1-1-onto-> Y )
6 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
7 5 6 syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> F : X --> Y )
8 7 frnd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ran F C_ Y )
9 1 8 sstrid 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F " ( P ( ball ` M ) R ) ) C_ Y )
10 9 sseld 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( x e. ( F " ( P ( ball ` M ) R ) ) -> x e. Y ) )
11 simpl2 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> N e. ( *Met ` Y ) )
12 simprl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> P e. X )
13 ffvelcdm 
 |-  ( ( F : X --> Y /\ P e. X ) -> ( F ` P ) e. Y )
14 7 12 13 syl2anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F ` P ) e. Y )
15 simprr 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> R e. RR* )
16 blssm 
 |-  ( ( N e. ( *Met ` Y ) /\ ( F ` P ) e. Y /\ R e. RR* ) -> ( ( F ` P ) ( ball ` N ) R ) C_ Y )
17 11 14 15 16 syl3anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( ( F ` P ) ( ball ` N ) R ) C_ Y )
18 17 sseld 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( x e. ( ( F ` P ) ( ball ` N ) R ) -> x e. Y ) )
19 simpl1 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> M e. ( *Met ` X ) )
20 19 adantr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> M e. ( *Met ` X ) )
21 simplrr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> R e. RR* )
22 simplrl 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> P e. X )
23 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
24 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
25 5 23 24 3syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> `' F : Y --> X )
26 ffvelcdm 
 |-  ( ( `' F : Y --> X /\ x e. Y ) -> ( `' F ` x ) e. X )
27 25 26 sylan 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( `' F ` x ) e. X )
28 elbl2 
 |-  ( ( ( M e. ( *Met ` X ) /\ R e. RR* ) /\ ( P e. X /\ ( `' F ` x ) e. X ) ) -> ( ( `' F ` x ) e. ( P ( ball ` M ) R ) <-> ( P M ( `' F ` x ) ) < R ) )
29 20 21 22 27 28 syl22anc 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( `' F ` x ) e. ( P ( ball ` M ) R ) <-> ( P M ( `' F ` x ) ) < R ) )
30 4 simprd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) )
31 oveq1 
 |-  ( x = P -> ( x M y ) = ( P M y ) )
32 fveq2 
 |-  ( x = P -> ( F ` x ) = ( F ` P ) )
33 32 oveq1d 
 |-  ( x = P -> ( ( F ` x ) N ( F ` y ) ) = ( ( F ` P ) N ( F ` y ) ) )
34 31 33 eqeq12d 
 |-  ( x = P -> ( ( x M y ) = ( ( F ` x ) N ( F ` y ) ) <-> ( P M y ) = ( ( F ` P ) N ( F ` y ) ) ) )
35 oveq2 
 |-  ( y = ( `' F ` x ) -> ( P M y ) = ( P M ( `' F ` x ) ) )
36 fveq2 
 |-  ( y = ( `' F ` x ) -> ( F ` y ) = ( F ` ( `' F ` x ) ) )
37 36 oveq2d 
 |-  ( y = ( `' F ` x ) -> ( ( F ` P ) N ( F ` y ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) )
38 35 37 eqeq12d 
 |-  ( y = ( `' F ` x ) -> ( ( P M y ) = ( ( F ` P ) N ( F ` y ) ) <-> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) ) )
39 34 38 rspc2v 
 |-  ( ( P e. X /\ ( `' F ` x ) e. X ) -> ( A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) -> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) ) )
40 39 impancom 
 |-  ( ( P e. X /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) -> ( ( `' F ` x ) e. X -> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) ) )
41 12 30 40 syl2anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( ( `' F ` x ) e. X -> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) ) )
42 41 imp 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ ( `' F ` x ) e. X ) -> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) )
43 27 42 syldan 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( P M ( `' F ` x ) ) = ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) )
44 43 breq1d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( P M ( `' F ` x ) ) < R <-> ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) < R ) )
45 29 44 bitrd 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( `' F ` x ) e. ( P ( ball ` M ) R ) <-> ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) < R ) )
46 f1of1 
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
47 5 46 syl 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> F : X -1-1-> Y )
48 47 adantr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> F : X -1-1-> Y )
49 blssm 
 |-  ( ( M e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` M ) R ) C_ X )
50 19 12 15 49 syl3anc 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( P ( ball ` M ) R ) C_ X )
51 50 adantr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( P ( ball ` M ) R ) C_ X )
52 f1elima 
 |-  ( ( F : X -1-1-> Y /\ ( `' F ` x ) e. X /\ ( P ( ball ` M ) R ) C_ X ) -> ( ( F ` ( `' F ` x ) ) e. ( F " ( P ( ball ` M ) R ) ) <-> ( `' F ` x ) e. ( P ( ball ` M ) R ) ) )
53 48 27 51 52 syl3anc 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( F " ( P ( ball ` M ) R ) ) <-> ( `' F ` x ) e. ( P ( ball ` M ) R ) ) )
54 11 adantr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> N e. ( *Met ` Y ) )
55 14 adantr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( F ` P ) e. Y )
56 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
57 5 56 sylan 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
58 simpr 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> x e. Y )
59 57 58 eqeltrd 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( F ` ( `' F ` x ) ) e. Y )
60 elbl2 
 |-  ( ( ( N e. ( *Met ` Y ) /\ R e. RR* ) /\ ( ( F ` P ) e. Y /\ ( F ` ( `' F ` x ) ) e. Y ) ) -> ( ( F ` ( `' F ` x ) ) e. ( ( F ` P ) ( ball ` N ) R ) <-> ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) < R ) )
61 54 21 55 59 60 syl22anc 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( ( F ` P ) ( ball ` N ) R ) <-> ( ( F ` P ) N ( F ` ( `' F ` x ) ) ) < R ) )
62 45 53 61 3bitr4d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( F " ( P ( ball ` M ) R ) ) <-> ( F ` ( `' F ` x ) ) e. ( ( F ` P ) ( ball ` N ) R ) ) )
63 57 eleq1d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( F " ( P ( ball ` M ) R ) ) <-> x e. ( F " ( P ( ball ` M ) R ) ) ) )
64 57 eleq1d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( ( F ` P ) ( ball ` N ) R ) <-> x e. ( ( F ` P ) ( ball ` N ) R ) ) )
65 62 63 64 3bitr3d 
 |-  ( ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) /\ x e. Y ) -> ( x e. ( F " ( P ( ball ` M ) R ) ) <-> x e. ( ( F ` P ) ( ball ` N ) R ) ) )
66 65 ex 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( x e. Y -> ( x e. ( F " ( P ( ball ` M ) R ) ) <-> x e. ( ( F ` P ) ( ball ` N ) R ) ) ) )
67 10 18 66 pm5.21ndd 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( x e. ( F " ( P ( ball ` M ) R ) ) <-> x e. ( ( F ` P ) ( ball ` N ) R ) ) )
68 67 eqrdv 
 |-  ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F " ( P ( ball ` M ) R ) ) = ( ( F ` P ) ( ball ` N ) R ) )