# 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}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
ismrer1.2 ${⊢}{F}=\left({x}\in ℝ⟼\left\{{A}\right\}×\left\{{x}\right\}\right)$
Assertion ismrer1 ${⊢}{A}\in {V}\to {F}\in \left({R}\mathrm{Ismty}{ℝ}^{n}\left(\left\{{A}\right\}\right)\right)$

### Proof

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