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 ∞Met X N ∞Met Y F M Ismty N P X R * F P ball M R = F P ball N R

Proof

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