Step | Hyp | Ref
| Expression |
1 | | sneq 4576 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → {𝑦} = {𝐴}) |
2 | 1 | xpeq1d 5617 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ({𝑦} × {𝑥}) = ({𝐴} × {𝑥})) |
3 | 2 | mpteq2dv 5180 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))) |
4 | | ismrer1.2 |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥})) |
5 | 3, 4 | eqtr4di 2797 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = 𝐹) |
6 | 5 | f1oeq1d 6707 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑m {𝑦}))) |
7 | 1 | oveq2d 7284 |
. . . . 5
⊢ (𝑦 = 𝐴 → (ℝ ↑m {𝑦}) = (ℝ ↑m
{𝐴})) |
8 | | f1oeq3 6702 |
. . . . 5
⊢ ((ℝ
↑m {𝑦}) =
(ℝ ↑m {𝐴}) → (𝐹:ℝ–1-1-onto→(ℝ ↑m {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}))) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝐹:ℝ–1-1-onto→(ℝ ↑m {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}))) |
10 | 6, 9 | bitrd 278 |
. . 3
⊢ (𝑦 = 𝐴 → ((𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m {𝑦}) ↔ 𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}))) |
11 | | eqid 2739 |
. . . 4
⊢ {𝑦} = {𝑦} |
12 | | reex 10946 |
. . . 4
⊢ ℝ
∈ V |
13 | | vex 3434 |
. . . 4
⊢ 𝑦 ∈ V |
14 | | eqid 2739 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) = (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})) |
15 | 11, 12, 13, 14 | mapsnf1o3 8657 |
. . 3
⊢ (𝑥 ∈ ℝ ↦ ({𝑦} × {𝑥})):ℝ–1-1-onto→(ℝ ↑m {𝑦}) |
16 | 10, 15 | vtoclg 3503 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴})) |
17 | | sneq 4576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
18 | 17 | xpeq2d 5618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ({𝐴} × {𝑥}) = ({𝐴} × {𝑦})) |
19 | | snex 5357 |
. . . . . . . . . . . . . . . . 17
⊢ {𝐴} ∈ V |
20 | | snex 5357 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥} ∈ V |
21 | 19, 20 | xpex 7594 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴} × {𝑥}) ∈ V |
22 | 18, 4, 21 | fvmpt3i 6874 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝐹‘𝑦) = ({𝐴} × {𝑦})) |
23 | 22 | fveq1d 6770 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → ((𝐹‘𝑦)‘𝐴) = (({𝐴} × {𝑦})‘𝐴)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑦)‘𝐴) = (({𝐴} × {𝑦})‘𝐴)) |
25 | | snidg 4600 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
26 | | fvconst2g 7071 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ V ∧ 𝐴 ∈ {𝐴}) → (({𝐴} × {𝑦})‘𝐴) = 𝑦) |
27 | 13, 25, 26 | sylancr 586 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (({𝐴} × {𝑦})‘𝐴) = 𝑦) |
28 | 24, 27 | sylan9eqr 2801 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦)‘𝐴) = 𝑦) |
29 | | sneq 4576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
30 | 29 | xpeq2d 5618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ({𝐴} × {𝑥}) = ({𝐴} × {𝑧})) |
31 | 30, 4, 21 | fvmpt3i 6874 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ → (𝐹‘𝑧) = ({𝐴} × {𝑧})) |
32 | 31 | fveq1d 6770 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℝ → ((𝐹‘𝑧)‘𝐴) = (({𝐴} × {𝑧})‘𝐴)) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑧)‘𝐴) = (({𝐴} × {𝑧})‘𝐴)) |
34 | | vex 3434 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
35 | | fvconst2g 7071 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ V ∧ 𝐴 ∈ {𝐴}) → (({𝐴} × {𝑧})‘𝐴) = 𝑧) |
36 | 34, 25, 35 | sylancr 586 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (({𝐴} × {𝑧})‘𝐴) = 𝑧) |
37 | 33, 36 | sylan9eqr 2801 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑧)‘𝐴) = 𝑧) |
38 | 28, 37 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴)) = (𝑦 − 𝑧)) |
39 | 38 | oveq1d 7283 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) = ((𝑦 − 𝑧)↑2)) |
40 | | resubcl 11268 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 − 𝑧) ∈ ℝ) |
41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦 − 𝑧) ∈ ℝ) |
42 | | absresq 14995 |
. . . . . . . . . . 11
⊢ ((𝑦 − 𝑧) ∈ ℝ → ((abs‘(𝑦 − 𝑧))↑2) = ((𝑦 − 𝑧)↑2)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑦 − 𝑧))↑2) = ((𝑦 − 𝑧)↑2)) |
44 | 39, 43 | eqtr4d 2782 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) = ((abs‘(𝑦 − 𝑧))↑2)) |
45 | 41 | recnd 10987 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦 − 𝑧) ∈ ℂ) |
46 | 45 | abscld 15129 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘(𝑦 − 𝑧)) ∈ ℝ) |
47 | 46 | recnd 10987 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘(𝑦 − 𝑧)) ∈ ℂ) |
48 | 47 | sqcld 13843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑦 − 𝑧))↑2) ∈ ℂ) |
49 | 44, 48 | eqeltrd 2840 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) ∈ ℂ) |
50 | | fveq2 6768 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ((𝐹‘𝑦)‘𝑘) = ((𝐹‘𝑦)‘𝐴)) |
51 | | fveq2 6768 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → ((𝐹‘𝑧)‘𝑘) = ((𝐹‘𝑧)‘𝐴)) |
52 | 50, 51 | oveq12d 7286 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘)) = (((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))) |
53 | 52 | oveq1d 7283 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
54 | 53 | sumsn 15439 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2) ∈ ℂ) →
Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
55 | 49, 54 | syldan 590 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((((𝐹‘𝑦)‘𝐴) − ((𝐹‘𝑧)‘𝐴))↑2)) |
56 | 55, 44 | eqtrd 2779 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2) = ((abs‘(𝑦 − 𝑧))↑2)) |
57 | 56 | fveq2d 6772 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘Σ𝑘
∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2)) =
(√‘((abs‘(𝑦 − 𝑧))↑2))) |
58 | 45 | absge0d 15137 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → 0 ≤
(abs‘(𝑦 − 𝑧))) |
59 | 46, 58 | sqrtsqd 15112 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘((abs‘(𝑦 − 𝑧))↑2)) = (abs‘(𝑦 − 𝑧))) |
60 | 57, 59 | eqtrd 2779 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) →
(√‘Σ𝑘
∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2)) = (abs‘(𝑦 − 𝑧))) |
61 | | f1of 6712 |
. . . . . . . 8
⊢ (𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}) → 𝐹:ℝ⟶(ℝ ↑m
{𝐴})) |
62 | 16, 61 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐹:ℝ⟶(ℝ ↑m
{𝐴})) |
63 | 62 | ffvelrnda 6955 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (ℝ ↑m {𝐴})) |
64 | 62 | ffvelrnda 6955 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) ∈ (ℝ ↑m {𝐴})) |
65 | 63, 64 | anim12dan 618 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦) ∈ (ℝ ↑m {𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑m {𝐴}))) |
66 | | snfi 8804 |
. . . . . 6
⊢ {𝐴} ∈ Fin |
67 | | eqid 2739 |
. . . . . . 7
⊢ (ℝ
↑m {𝐴}) =
(ℝ ↑m {𝐴}) |
68 | 67 | rrnmval 35965 |
. . . . . 6
⊢ (({𝐴} ∈ Fin ∧ (𝐹‘𝑦) ∈ (ℝ ↑m {𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑m {𝐴})) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
69 | 66, 68 | mp3an1 1446 |
. . . . 5
⊢ (((𝐹‘𝑦) ∈ (ℝ ↑m {𝐴}) ∧ (𝐹‘𝑧) ∈ (ℝ ↑m {𝐴})) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
70 | 65, 69 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)) = (√‘Σ𝑘 ∈ {𝐴} ((((𝐹‘𝑦)‘𝑘) − ((𝐹‘𝑧)‘𝑘))↑2))) |
71 | | ismrer1.1 |
. . . . . 6
⊢ 𝑅 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
72 | 71 | remetdval 23933 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦𝑅𝑧) = (abs‘(𝑦 − 𝑧))) |
73 | 72 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦𝑅𝑧) = (abs‘(𝑦 − 𝑧))) |
74 | 60, 70, 73 | 3eqtr4rd 2790 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))) |
75 | 74 | ralrimivva 3116 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))) |
76 | 71 | rexmet 23935 |
. . 3
⊢ 𝑅 ∈
(∞Met‘ℝ) |
77 | 67 | rrnmet 35966 |
. . . 4
⊢ ({𝐴} ∈ Fin →
(ℝn‘{𝐴}) ∈ (Met‘(ℝ
↑m {𝐴}))) |
78 | | metxmet 23468 |
. . . 4
⊢
((ℝn‘{𝐴}) ∈ (Met‘(ℝ
↑m {𝐴}))
→ (ℝn‘{𝐴}) ∈ (∞Met‘(ℝ
↑m {𝐴}))) |
79 | 66, 77, 78 | mp2b 10 |
. . 3
⊢
(ℝn‘{𝐴}) ∈ (∞Met‘(ℝ
↑m {𝐴})) |
80 | | isismty 35938 |
. . 3
⊢ ((𝑅 ∈
(∞Met‘ℝ) ∧ (ℝn‘{𝐴}) ∈
(∞Met‘(ℝ ↑m {𝐴}))) → (𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴})) ↔ (𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧))))) |
81 | 76, 79, 80 | mp2an 688 |
. 2
⊢ (𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴})) ↔ (𝐹:ℝ–1-1-onto→(ℝ ↑m {𝐴}) ∧ ∀𝑦 ∈ ℝ ∀𝑧 ∈ ℝ (𝑦𝑅𝑧) = ((𝐹‘𝑦)(ℝn‘{𝐴})(𝐹‘𝑧)))) |
82 | 16, 75, 81 | sylanbrc 582 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty
(ℝn‘{𝐴}))) |