Step | Hyp | Ref
| Expression |
1 | | sneq 4408 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → {𝑦} = {𝐴}) |
2 | 1 | xpeq1d 5384 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ({𝑦} × {𝑥}) = ({𝐴} × {𝑥})) |
3 | 2 | mpteq2dv 4980 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))) |
4 | | ismrer1.2 |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥})) |
5 | 3, 4 | syl6eqr 2832 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = 𝐹) |
6 | | f1oeq1 6380 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = 𝐹 → ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}))) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}))) |
8 | 1 | oveq2d 6938 |
. . . . 5
⊢ (𝑦 = 𝐴 → (ℝ ↑𝑚
{𝑦}) = (ℝ
↑𝑚 {𝐴})) |
9 | | f1oeq3 6382 |
. . . . 5
⊢ ((ℝ
↑𝑚 {𝑦}) = (ℝ ↑𝑚
{𝐴}) → (𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}))) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}))) |
11 | 7, 10 | bitrd 271 |
. . 3
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}))) |
12 | | eqid 2778 |
. . . 4
⊢ {𝑦} = {𝑦} |
13 | | reex 10363 |
. . . 4
⊢ ℝ
∈ V |
14 | | vex 3401 |
. . . 4
⊢ 𝑦 ∈ V |
15 | | eqid 2778 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) |
16 | 12, 13, 14, 15 | mapsnf1o3 8192 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑𝑚 {𝑦}) |
17 | 11, 16 | vtoclg 3467 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴})) |
18 | | sneq 4408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
19 | 18 | xpeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ({𝐴} × {𝑥}) = ({𝐴} × {𝑦})) |
20 | | snex 5140 |
. . . . . . . . . . . . . . . . 17
⊢ {𝐴} ∈ V |
21 | | snex 5140 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ V |
22 | 20, 21 | xpex 7240 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴} × {𝑥}) ∈ V |
23 | 19, 4, 22 | fvmpt3i 6547 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝐹‘𝑦) = ({𝐴} × {𝑦})) |
24 | 23 | fveq1d 6448 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → ((𝐹‘𝑦)‘𝐴) = (({𝐴} × {𝑦})‘𝐴)) |
25 | 24 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑦)‘𝐴) = (({𝐴} × {𝑦})‘𝐴)) |
26 | | snidg 4428 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
27 | | fvconst2g 6739 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ V ∧ 𝐴 ∈ {𝐴}) → (({𝐴} × {𝑦})‘𝐴) = 𝑦) |
28 | 14, 26, 27 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (({𝐴} × {𝑦})‘𝐴) = 𝑦) |
29 | 25, 28 | sylan9eqr 2836 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦)‘𝐴) = 𝑦) |
30 | | sneq 4408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
31 | 30 | xpeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ({𝐴} × {𝑥}) = ({𝐴} × {𝑧})) |
32 | 31, 4, 22 | fvmpt3i 6547 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝐹‘𝑧) = ({𝐴} × {𝑧})) |
33 | 32 | fveq1d 6448 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ → ((𝐹‘𝑧)‘𝐴) = (({𝐴} × {𝑧})‘𝐴)) |
34 | 33 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑧)‘𝐴) = (({𝐴} × {𝑧})‘𝐴)) |
35 | | vex 3401 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
36 | | fvconst2g 6739 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ V ∧ 𝐴 ∈ {𝐴}) → (({𝐴} × {𝑧})‘𝐴) = 𝑧) |
37 | 35, 26, 36 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (({𝐴} × {𝑧})‘𝐴) = 𝑧) |
38 | 34, 37 | sylan9eqr 2836 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑧)‘𝐴) = 𝑧) |
39 | 29, 38 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴)) = (𝑦 − 𝑧)) |
40 | 39 | oveq1d 6937 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) = ((𝑦 − 𝑧)↑2)) |
41 | | resubcl 10687 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 − 𝑧) ∈ ℝ) |
42 | 41 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦 − 𝑧) ∈ ℝ) |
43 | | absresq 14449 |
. . . . . . . . . . 11
⊢ ((𝑦 − 𝑧) ∈ ℝ → ((abs‘(𝑦 − 𝑧))↑2) = ((𝑦 − 𝑧)↑2)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑦 − 𝑧))↑2) = ((𝑦 − 𝑧)↑2)) |
45 | 40, 44 | eqtr4d 2817 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) = ((abs‘(𝑦 − 𝑧))↑2)) |
46 | 42 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦 − 𝑧) ∈ ℂ) |
47 | 46 | abscld 14583 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘(𝑦 − 𝑧)) ∈ ℝ) |
48 | 47 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘(𝑦 − 𝑧)) ∈ ℂ) |
49 | 48 | sqcld 13325 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑦 − 𝑧))↑2) ∈ ℂ) |
50 | 45, 49 | eqeltrd 2859 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) ∈ ℂ) |
51 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑦)‘𝐴)) |
52 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ((𝐹‘𝑧)‘𝑘) = ((𝐹‘𝑧)‘𝐴)) |
53 | 51, 52 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘)) = (((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))) |
54 | 53 | oveq1d 6937 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
55 | 54 | sumsn 14882 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) ∈ ℂ) →
Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
56 | 50, 55 | syldan 585 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
57 | 56, 45 | eqtrd 2814 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((abs‘(𝑦 − 𝑧))↑2)) |
58 | 57 | fveq2d 6450 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘Σ𝑘
∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2)) =
(√‘((abs‘(𝑦 − 𝑧))↑2))) |
59 | 46 | absge0d 14591 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → 0 ≤
(abs‘(𝑦 − 𝑧))) |
60 | 47, 59 | sqrtsqd 14566 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘((abs‘(𝑦 − 𝑧))↑2)) = (abs‘(𝑦 − 𝑧))) |
61 | 58, 60 | eqtrd 2814 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘Σ𝑘
∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2)) = (abs‘(𝑦 − 𝑧))) |
62 | | f1of 6391 |
. . . . . . . 8
⊢ (𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}) → 𝐹:ℝ⟶(ℝ
↑𝑚 {𝐴})) |
63 | 17, 62 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐹:ℝ⟶(ℝ
↑𝑚 {𝐴})) |
64 | 63 | ffvelrnda 6623 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (ℝ ↑𝑚
{𝐴})) |
65 | 63 | ffvelrnda 6623 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) ∈ (ℝ ↑𝑚
{𝐴})) |
66 | 64, 65 | anim12dan 612 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦) ∈ (ℝ ↑𝑚
{𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑𝑚
{𝐴}))) |
67 | | snfi 8326 |
. . . . . 6
⊢ {𝐴} ∈ Fin |
68 | | eqid 2778 |
. . . . . . 7
⊢ (ℝ
↑𝑚 {𝐴}) = (ℝ ↑𝑚
{𝐴}) |
69 | 68 | rrnmval 34251 |
. . . . . 6
⊢ (({𝐴} ∈ Fin ∧ (𝐹‘𝑦) ∈ (ℝ ↑𝑚
{𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑𝑚
{𝐴})) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
70 | 67, 69 | mp3an1 1521 |
. . . . 5
⊢ (((𝐹‘𝑦) ∈ (ℝ ↑𝑚
{𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑𝑚
{𝐴})) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
71 | 66, 70 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
72 | | ismrer1.1 |
. . . . . 6
⊢ 𝑅 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
73 | 72 | remetdval 23000 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦𝑅𝑧) = (abs‘(𝑦 − 𝑧))) |
74 | 73 | adantl 475 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦𝑅𝑧) = (abs‘(𝑦 − 𝑧))) |
75 | 61, 71, 74 | 3eqtr4rd 2825 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))) |
76 | 75 | ralrimivva 3153 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))) |
77 | 72 | rexmet 23002 |
. . 3
⊢ 𝑅 ∈
(∞Met‘ℝ) |
78 | 68 | rrnmet 34252 |
. . . 4
⊢ ({𝐴} ∈ Fin →
(ℝn‘{𝐴}) ∈ (Met‘(ℝ
↑𝑚 {𝐴}))) |
79 | | metxmet 22547 |
. . . 4
⊢
((ℝn‘{𝐴}) ∈ (Met‘(ℝ
↑𝑚 {𝐴})) →
(ℝn‘{𝐴}) ∈ (∞Met‘(ℝ
↑𝑚 {𝐴}))) |
80 | 67, 78, 79 | mp2b 10 |
. . 3
⊢
(ℝn‘{𝐴}) ∈ (∞Met‘(ℝ
↑𝑚 {𝐴})) |
81 | | isismty 34224 |
. . 3
⊢ ((𝑅 ∈
(∞Met‘ℝ) ∧ (ℝn‘{𝐴}) ∈
(∞Met‘(ℝ ↑𝑚 {𝐴}))) → (𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴})) ↔ (𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))))) |
82 | 77, 80, 81 | mp2an 682 |
. 2
⊢ (𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴})) ↔ (𝐹:ℝ–1-1-onto→(ℝ ↑𝑚 {𝐴}) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)))) |
83 | 17, 76, 82 | sylanbrc 578 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴}))) |