Metamath Proof Explorer


Theorem ismrer1

Description: An isometry between RR and RR ^ 1 . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses ismrer1.1 R = abs 2
ismrer1.2 F = x A × x
Assertion ismrer1 A V F R Ismty n A

Proof

Step Hyp Ref Expression
1 ismrer1.1 R = abs 2
2 ismrer1.2 F = x A × x
3 sneq y = A y = A
4 3 xpeq1d y = A y × x = A × x
5 4 mpteq2dv y = A x y × x = x A × x
6 5 2 eqtr4di y = A x y × x = F
7 6 f1oeq1d y = A x y × x : 1-1 onto y F : 1-1 onto y
8 3 oveq2d y = A y = A
9 f1oeq3 y = A F : 1-1 onto y F : 1-1 onto A
10 8 9 syl y = A F : 1-1 onto y F : 1-1 onto A
11 7 10 bitrd y = A x y × x : 1-1 onto y F : 1-1 onto A
12 eqid y = y
13 reex V
14 vex y V
15 eqid x y × x = x y × x
16 12 13 14 15 mapsnf1o3 x y × x : 1-1 onto y
17 11 16 vtoclg A V F : 1-1 onto A
18 sneq x = y x = y
19 18 xpeq2d x = y A × x = A × y
20 snex A V
21 snex x V
22 20 21 xpex A × x V
23 19 2 22 fvmpt3i y F y = A × y
24 23 fveq1d y F y A = A × y A
25 24 adantr y z F y A = A × y A
26 snidg A V A A
27 fvconst2g y V A A A × y A = y
28 14 26 27 sylancr A V A × y A = y
29 25 28 sylan9eqr A V y z F y A = y
30 sneq x = z x = z
31 30 xpeq2d x = z A × x = A × z
32 31 2 22 fvmpt3i z F z = A × z
33 32 fveq1d z F z A = A × z A
34 33 adantl y z F z A = A × z A
35 vex z V
36 fvconst2g z V A A A × z A = z
37 35 26 36 sylancr A V A × z A = z
38 34 37 sylan9eqr A V y z F z A = z
39 29 38 oveq12d A V y z F y A F z A = y z
40 39 oveq1d A V y z F y A F z A 2 = y z 2
41 resubcl y z y z
42 41 adantl A V y z y z
43 absresq y z y z 2 = y z 2
44 42 43 syl A V y z y z 2 = y z 2
45 40 44 eqtr4d A V y z F y A F z A 2 = y z 2
46 42 recnd A V y z y z
47 46 abscld A V y z y z
48 47 recnd A V y z y z
49 48 sqcld A V y z y z 2
50 45 49 eqeltrd A V y z F y A F z A 2
51 fveq2 k = A F y k = F y A
52 fveq2 k = A F z k = F z A
53 51 52 oveq12d k = A F y k F z k = F y A F z A
54 53 oveq1d k = A F y k F z k 2 = F y A F z A 2
55 54 sumsn A V F y A F z A 2 k A F y k F z k 2 = F y A F z A 2
56 50 55 syldan A V y z k A F y k F z k 2 = F y A F z A 2
57 56 45 eqtrd A V y z k A F y k F z k 2 = y z 2
58 57 fveq2d A V y z k A F y k F z k 2 = y z 2
59 46 absge0d A V y z 0 y z
60 47 59 sqrtsqd A V y z y z 2 = y z
61 58 60 eqtrd A V y z k A F y k F z k 2 = y z
62 f1of F : 1-1 onto A F : A
63 17 62 syl A V F : A
64 63 ffvelrnda A V y F y A
65 63 ffvelrnda A V z F z A
66 64 65 anim12dan A V y z F y A F z A
67 snfi A Fin
68 eqid A = A
69 68 rrnmval A Fin F y A F z A F y n A F z = k A F y k F z k 2
70 67 69 mp3an1 F y A F z A F y n A F z = k A F y k F z k 2
71 66 70 syl A V y z F y n A F z = k A F y k F z k 2
72 1 remetdval y z y R z = y z
73 72 adantl A V y z y R z = y z
74 61 71 73 3eqtr4rd A V y z y R z = F y n A F z
75 74 ralrimivva A V y z y R z = F y n A F z
76 1 rexmet R ∞Met
77 68 rrnmet A Fin n A Met A
78 metxmet n A Met A n A ∞Met A
79 67 77 78 mp2b n A ∞Met A
80 isismty R ∞Met n A ∞Met A F R Ismty n A F : 1-1 onto A y z y R z = F y n A F z
81 76 79 80 mp2an F R Ismty n A F : 1-1 onto A y z y R z = F y n A F z
82 17 75 81 sylanbrc A V F R Ismty n A