Step | Hyp | Ref
| Expression |
1 | | minveco.x |
. . 3
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | minveco.m |
. . 3
⊢ 𝑀 = ( −𝑣
‘𝑈) |
3 | | minveco.n |
. . 3
⊢ 𝑁 =
(normCV‘𝑈) |
4 | | minveco.y |
. . 3
⊢ 𝑌 = (BaseSet‘𝑊) |
5 | | minveco.u |
. . 3
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) |
6 | | minveco.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) |
7 | | minveco.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | minveco.d |
. . 3
⊢ 𝐷 = (IndMet‘𝑈) |
9 | | minveco.j |
. . 3
⊢ 𝐽 = (MetOpen‘𝐷) |
10 | | minveco.r |
. . 3
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
11 | | minveco.s |
. . 3
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minvecolem5 29237 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
13 | 5 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑈 ∈
CPreHilOLD) |
14 | 6 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) |
15 | 7 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝐴 ∈ 𝑋) |
16 | | 0re 10976 |
. . . . . . 7
⊢ 0 ∈
ℝ |
17 | 16 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ∈
ℝ) |
18 | | 0le0 12072 |
. . . . . . 7
⊢ 0 ≤
0 |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ≤
0) |
20 | | simplrl 774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑥 ∈ 𝑌) |
21 | | simplrr 775 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑤 ∈ 𝑌) |
22 | | simprl 768 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0)) |
23 | | simprr 770 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) |
24 | 1, 2, 3, 4, 13, 14, 15, 8, 9, 10, 11, 17, 19, 20, 21, 22, 23 | minvecolem2 29231 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0)) |
25 | 24 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0))) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minvecolem6 29238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
27 | 26 | adantrr 714 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
28 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minvecolem6 29238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
29 | 28 | adantrl 713 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
30 | 27, 29 | anbi12d 631 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) ↔ (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))))) |
31 | | 4cn 12056 |
. . . . . . 7
⊢ 4 ∈
ℂ |
32 | 31 | mul01i 11163 |
. . . . . 6
⊢ (4
· 0) = 0 |
33 | 32 | breq2i 5087 |
. . . . 5
⊢ (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ ((𝑥𝐷𝑤)↑2) ≤ 0) |
34 | | phnv 29170 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
35 | 5, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ NrmCVec) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑈 ∈ NrmCVec) |
37 | 1, 8 | imsmet 29047 |
. . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝐷 ∈ (Met‘𝑋)) |
39 | | inss1 4168 |
. . . . . . . . . . . . 13
⊢
((SubSp‘𝑈)
∩ CBan) ⊆ (SubSp‘𝑈) |
40 | 39, 6 | sselid 3924 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) |
41 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
42 | 1, 4, 41 | sspba 29083 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) |
43 | 35, 40, 42 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑌 ⊆ 𝑋) |
45 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑌) |
46 | 44, 45 | sseldd 3927 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
47 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌) |
48 | 44, 47 | sseldd 3927 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑋) |
49 | | metcl 23481 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑥𝐷𝑤) ∈ ℝ) |
50 | 38, 46, 48, 49 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℝ) |
51 | 50 | sqge0d 13962 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 0 ≤ ((𝑥𝐷𝑤)↑2)) |
52 | 51 | biantrud 532 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
53 | 50 | resqcld 13961 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑥𝐷𝑤)↑2) ∈ ℝ) |
54 | | letri3 11059 |
. . . . . . 7
⊢ ((((𝑥𝐷𝑤)↑2) ∈ ℝ ∧ 0 ∈
ℝ) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
55 | 53, 16, 54 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) |
56 | 50 | recnd 11002 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℂ) |
57 | | sqeq0 13836 |
. . . . . . . 8
⊢ ((𝑥𝐷𝑤) ∈ ℂ → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) |
59 | | meteq0 23488 |
. . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝑥𝐷𝑤) = 0 ↔ 𝑥 = 𝑤)) |
60 | 38, 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 | 33, 62 | syl5bb 283 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ 𝑥 = 𝑤)) |
64 | 25, 30, 63 | 3imtr3d 293 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤)) |
65 | 64 | ralrimivva 3117 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤)) |
66 | | oveq2 7277 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (𝐴𝑀𝑥) = (𝐴𝑀𝑤)) |
67 | 66 | fveq2d 6773 |
. . . . 5
⊢ (𝑥 = 𝑤 → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀𝑤))) |
68 | 67 | breq1d 5089 |
. . . 4
⊢ (𝑥 = 𝑤 → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
69 | 68 | ralbidv 3123 |
. . 3
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
70 | 69 | reu4 3670 |
. 2
⊢
(∃!𝑥 ∈
𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤))) |
71 | 12, 65, 70 | sylanbrc 583 |
1
⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |