Metamath Proof Explorer


Theorem ismtyval

Description: The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ismtyval M ∞Met X N ∞Met Y M Ismty N = f | f : X 1-1 onto Y x X y X x M y = f x N f y

Proof

Step Hyp Ref Expression
1 df-ismty Ismty = m ran ∞Met , n ran ∞Met f | f : dom dom m 1-1 onto dom dom n x dom dom m y dom dom m x m y = f x n f y
2 1 a1i M ∞Met X N ∞Met Y Ismty = m ran ∞Met , n ran ∞Met f | f : dom dom m 1-1 onto dom dom n x dom dom m y dom dom m x m y = f x n f y
3 dmeq m = M dom m = dom M
4 xmetf M ∞Met X M : X × X *
5 4 fdmd M ∞Met X dom M = X × X
6 3 5 sylan9eqr M ∞Met X m = M dom m = X × X
7 6 ad2ant2r M ∞Met X N ∞Met Y m = M n = N dom m = X × X
8 7 dmeqd M ∞Met X N ∞Met Y m = M n = N dom dom m = dom X × X
9 dmxpid dom X × X = X
10 8 9 eqtrdi M ∞Met X N ∞Met Y m = M n = N dom dom m = X
11 10 f1oeq2d M ∞Met X N ∞Met Y m = M n = N f : dom dom m 1-1 onto dom dom n f : X 1-1 onto dom dom n
12 dmeq n = N dom n = dom N
13 xmetf N ∞Met Y N : Y × Y *
14 13 fdmd N ∞Met Y dom N = Y × Y
15 12 14 sylan9eqr N ∞Met Y n = N dom n = Y × Y
16 15 ad2ant2l M ∞Met X N ∞Met Y m = M n = N dom n = Y × Y
17 16 dmeqd M ∞Met X N ∞Met Y m = M n = N dom dom n = dom Y × Y
18 dmxpid dom Y × Y = Y
19 17 18 eqtrdi M ∞Met X N ∞Met Y m = M n = N dom dom n = Y
20 f1oeq3 dom dom n = Y f : X 1-1 onto dom dom n f : X 1-1 onto Y
21 19 20 syl M ∞Met X N ∞Met Y m = M n = N f : X 1-1 onto dom dom n f : X 1-1 onto Y
22 11 21 bitrd M ∞Met X N ∞Met Y m = M n = N f : dom dom m 1-1 onto dom dom n f : X 1-1 onto Y
23 oveq m = M x m y = x M y
24 oveq n = N f x n f y = f x N f y
25 23 24 eqeqan12d m = M n = N x m y = f x n f y x M y = f x N f y
26 25 adantl M ∞Met X N ∞Met Y m = M n = N x m y = f x n f y x M y = f x N f y
27 10 26 raleqbidv M ∞Met X N ∞Met Y m = M n = N y dom dom m x m y = f x n f y y X x M y = f x N f y
28 10 27 raleqbidv M ∞Met X N ∞Met Y m = M n = N x dom dom m y dom dom m x m y = f x n f y x X y X x M y = f x N f y
29 22 28 anbi12d M ∞Met X N ∞Met Y m = M n = N f : dom dom m 1-1 onto dom dom n x dom dom m y dom dom m x m y = f x n f y f : X 1-1 onto Y x X y X x M y = f x N f y
30 29 abbidv M ∞Met X N ∞Met Y m = M n = N f | f : dom dom m 1-1 onto dom dom n x dom dom m y dom dom m x m y = f x n f y = f | f : X 1-1 onto Y x X y X x M y = f x N f y
31 fvssunirn ∞Met X ran ∞Met
32 simpl M ∞Met X N ∞Met Y M ∞Met X
33 31 32 sseldi M ∞Met X N ∞Met Y M ran ∞Met
34 fvssunirn ∞Met Y ran ∞Met
35 simpr M ∞Met X N ∞Met Y N ∞Met Y
36 34 35 sseldi M ∞Met X N ∞Met Y N ran ∞Met
37 f1of f : X 1-1 onto Y f : X Y
38 37 adantr f : X 1-1 onto Y x X y X x M y = f x N f y f : X Y
39 elfvdm N ∞Met Y Y dom ∞Met
40 elfvdm M ∞Met X X dom ∞Met
41 elmapg Y dom ∞Met X dom ∞Met f Y X f : X Y
42 39 40 41 syl2anr M ∞Met X N ∞Met Y f Y X f : X Y
43 38 42 syl5ibr M ∞Met X N ∞Met Y f : X 1-1 onto Y x X y X x M y = f x N f y f Y X
44 43 abssdv M ∞Met X N ∞Met Y f | f : X 1-1 onto Y x X y X x M y = f x N f y Y X
45 ovex Y X V
46 45 ssex f | f : X 1-1 onto Y x X y X x M y = f x N f y Y X f | f : X 1-1 onto Y x X y X x M y = f x N f y V
47 44 46 syl M ∞Met X N ∞Met Y f | f : X 1-1 onto Y x X y X x M y = f x N f y V
48 2 30 33 36 47 ovmpod M ∞Met X N ∞Met Y M Ismty N = f | f : X 1-1 onto Y x X y X x M y = f x N f y