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 o. - ) |` ( RR X. RR ) )
ismrer1.2 
|- F = ( x e. RR |-> ( { A } X. { x } ) )
Assertion ismrer1 
|- ( A e. V -> F e. ( R Ismty ( Rn ` { A } ) ) )

Proof

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