Step | Hyp | Ref
| Expression |
1 | | minvec.x |
. . 3
⊢ 𝑋 = (Base‘𝑈) |
2 | | minvec.m |
. . 3
⊢ − =
(-g‘𝑈) |
3 | | minvec.n |
. . 3
⊢ 𝑁 = (norm‘𝑈) |
4 | | minvec.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) |
5 | | minvec.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) |
6 | | minvec.w |
. . 3
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) |
7 | | minvec.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | minvec.j |
. . 3
⊢ 𝐽 = (TopOpen‘𝑈) |
9 | | minvec.r |
. . 3
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
10 | | minvec.s |
. . 3
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
11 | | minvec.d |
. . 3
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minveclem5 24597 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
13 | 4 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑈 ∈ ℂPreHil) |
14 | 5 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑌 ∈ (LSubSp‘𝑈)) |
15 | 6 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → (𝑈 ↾s 𝑌) ∈ CMetSp) |
16 | 7 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝐴 ∈ 𝑋) |
17 | | 0re 10977 |
. . . . . . 7
⊢ 0 ∈
ℝ |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ∈
ℝ) |
19 | | 0le0 12074 |
. . . . . . 7
⊢ 0 ≤
0 |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ≤
0) |
21 | | simplrl 774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑥 ∈ 𝑌) |
22 | | simplrr 775 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑤 ∈ 𝑌) |
23 | | simprl 768 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0)) |
24 | | simprr 770 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) |
25 | 1, 2, 3, 13, 14, 15, 16, 8, 9, 10, 11, 18, 20, 21, 22, 23, 24 | minveclem2 24590 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0)) |
26 | 25 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0))) |
27 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minveclem6 24598 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
28 | 27 | adantrr 714 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minveclem6 24598 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
30 | 29 | adantrl 713 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
31 | 28, 30 | anbi12d 631 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) ↔ (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦))))) |
32 | | 4cn 12058 |
. . . . . . 7
⊢ 4 ∈
ℂ |
33 | 32 | mul01i 11165 |
. . . . . 6
⊢ (4
· 0) = 0 |
34 | 33 | breq2i 5082 |
. . . . 5
⊢ (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ ((𝑥𝐷𝑤)↑2) ≤ 0) |
35 | | cphngp 24337 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
36 | | ngpms 23756 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) |
37 | 4, 35, 36 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ MetSp) |
38 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑈 ∈ MetSp) |
39 | 1, 11 | msmet 23610 |
. . . . . . . . . 10
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝐷 ∈ (Met‘𝑋)) |
41 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
42 | 1, 41 | lssss 20198 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
43 | 5, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑌 ⊆ 𝑋) |
45 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑌) |
46 | 44, 45 | sseldd 3922 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
47 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌) |
48 | 44, 47 | sseldd 3922 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑋) |
49 | | metcl 23485 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑥𝐷𝑤) ∈ ℝ) |
50 | 40, 46, 48, 49 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℝ) |
51 | 50 | sqge0d 13966 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 0 ≤ ((𝑥𝐷𝑤)↑2)) |
52 | 51 | biantrud 532 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
53 | 50 | resqcld 13965 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑥𝐷𝑤)↑2) ∈ ℝ) |
54 | | letri3 11060 |
. . . . . . 7
⊢ ((((𝑥𝐷𝑤)↑2) ∈ ℝ ∧ 0 ∈
ℝ) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
55 | 53, 17, 54 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
56 | 50 | recnd 11003 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℂ) |
57 | | sqeq0 13840 |
. . . . . . . 8
⊢ ((𝑥𝐷𝑤) ∈ ℂ → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) |
59 | | meteq0 23492 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝑥𝐷𝑤) = 0 ↔ 𝑥 = 𝑤)) |
60 | 40, 46, 48, 59 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑥𝐷𝑤) = 0 ↔ 𝑥 = 𝑤)) |
61 | 58, 60 | bitrd 278 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ 𝑥 = 𝑤)) |
62 | 52, 55, 61 | 3bitr2d 307 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ 0 ↔ 𝑥 = 𝑤)) |
63 | 34, 62 | bitrid 282 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ 𝑥 = 𝑤)) |
64 | 26, 31, 63 | 3imtr3d 293 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦))) → 𝑥 = 𝑤)) |
65 | 64 | ralrimivva 3123 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦))) → 𝑥 = 𝑤)) |
66 | | oveq2 7283 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝐴 − 𝑥) = (𝐴 − 𝑤)) |
67 | 66 | fveq2d 6778 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝑁‘(𝐴 − 𝑥)) = (𝑁‘(𝐴 − 𝑤))) |
68 | 67 | breq1d 5084 |
. . . 4
⊢ (𝑥 = 𝑤 → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
69 | 68 | ralbidv 3112 |
. . 3
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
70 | 69 | reu4 3666 |
. 2
⊢
(∃!𝑥 ∈
𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ∧ ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑤)) ≤ (𝑁‘(𝐴 − 𝑦))) → 𝑥 = 𝑤))) |
71 | 12, 65, 70 | sylanbrc 583 |
1
⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |