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 ⊢ 𝑅 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
ismrer1.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( { 𝐴 } × { 𝑥 } ) )
Assertion ismrer1 ( 𝐴 ∈ 𝑉 → 𝐹 ∈ ( 𝑅 Ismty ( ℝn ‘ { 𝐴 } ) ) )

Proof

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