| 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 30900 | . 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | 
| 13 | 5 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑈 ∈
CPreHilOLD) | 
| 14 | 6 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) | 
| 15 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝐴 ∈ 𝑋) | 
| 16 |  | 0re 11263 | . . . . . . 7
⊢ 0 ∈
ℝ | 
| 17 | 16 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ∈
ℝ) | 
| 18 |  | 0le0 12367 | . . . . . . 7
⊢ 0 ≤
0 | 
| 19 | 18 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 0 ≤
0) | 
| 20 |  | simplrl 777 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑥 ∈ 𝑌) | 
| 21 |  | simplrr 778 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → 𝑤 ∈ 𝑌) | 
| 22 |  | simprl 771 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0)) | 
| 23 |  | simprr 773 | . . . . . 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 30894 | . . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) ∧ (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0))) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0)) | 
| 25 | 24 | ex 412 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) → ((𝑥𝐷𝑤)↑2) ≤ (4 ·
0))) | 
| 26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minvecolem6 30901 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 27 | 26 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 28 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minvecolem6 30901 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 29 | 28 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 30 | 27, 29 | anbi12d 632 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ∧ ((𝐴𝐷𝑤)↑2) ≤ ((𝑆↑2) + 0)) ↔ (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))))) | 
| 31 |  | 4cn 12351 | . . . . . . 7
⊢ 4 ∈
ℂ | 
| 32 | 31 | mul01i 11451 | . . . . . 6
⊢ (4
· 0) = 0 | 
| 33 | 32 | breq2i 5151 | . . . . 5
⊢ (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ ((𝑥𝐷𝑤)↑2) ≤ 0) | 
| 34 |  | phnv 30833 | . . . . . . . . . . . 12
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) | 
| 35 | 5, 34 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ NrmCVec) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑈 ∈ NrmCVec) | 
| 37 | 1, 8 | imsmet 30710 | . . . . . . . . . 10
⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋)) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝐷 ∈ (Met‘𝑋)) | 
| 39 |  | inss1 4237 | . . . . . . . . . . . . 13
⊢
((SubSp‘𝑈)
∩ CBan) ⊆ (SubSp‘𝑈) | 
| 40 | 39, 6 | sselid 3981 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) | 
| 41 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) | 
| 42 | 1, 4, 41 | sspba 30746 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) | 
| 43 | 35, 40, 42 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ⊆ 𝑋) | 
| 44 | 43 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑌 ⊆ 𝑋) | 
| 45 |  | simprl 771 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑌) | 
| 46 | 44, 45 | sseldd 3984 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑥 ∈ 𝑋) | 
| 47 |  | simprr 773 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌) | 
| 48 | 44, 47 | sseldd 3984 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑋) | 
| 49 |  | metcl 24342 | . . . . . . . . 9
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑥𝐷𝑤) ∈ ℝ) | 
| 50 | 38, 46, 48, 49 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℝ) | 
| 51 | 50 | sqge0d 14177 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 0 ≤ ((𝑥𝐷𝑤)↑2)) | 
| 52 | 51 | biantrud 531 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ 0 ↔ (((𝑥𝐷𝑤)↑2) ≤ 0 ∧ 0 ≤ ((𝑥𝐷𝑤)↑2)))) | 
| 53 | 50 | resqcld 14165 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑥𝐷𝑤)↑2) ∈ ℝ) | 
| 54 |  | letri3 11346 | . . . . . . 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 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑥𝐷𝑤) ∈ ℂ) | 
| 57 |  | sqeq0 14160 | . . . . . . . 8
⊢ ((𝑥𝐷𝑤) ∈ ℂ → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) | 
| 58 | 56, 57 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ (𝑥𝐷𝑤) = 0)) | 
| 59 |  | meteq0 24349 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝑥𝐷𝑤) = 0 ↔ 𝑥 = 𝑤)) | 
| 60 | 38, 46, 48, 59 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑥𝐷𝑤) = 0 ↔ 𝑥 = 𝑤)) | 
| 61 | 58, 60 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) = 0 ↔ 𝑥 = 𝑤)) | 
| 62 | 52, 55, 61 | 3bitr2d 307 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ 0 ↔ 𝑥 = 𝑤)) | 
| 63 | 33, 62 | bitrid 283 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (((𝑥𝐷𝑤)↑2) ≤ (4 · 0) ↔ 𝑥 = 𝑤)) | 
| 64 | 25, 30, 63 | 3imtr3d 293 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤)) | 
| 65 | 64 | ralrimivva 3202 | . 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤)) | 
| 66 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = 𝑤 → (𝐴𝑀𝑥) = (𝐴𝑀𝑤)) | 
| 67 | 66 | fveq2d 6910 | . . . . 5
⊢ (𝑥 = 𝑤 → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀𝑤))) | 
| 68 | 67 | breq1d 5153 | . . . 4
⊢ (𝑥 = 𝑤 → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 69 | 68 | ralbidv 3178 | . . 3
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | 
| 70 | 69 | reu4 3737 | . 2
⊢
(∃!𝑥 ∈
𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑥 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ∧ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑤)) ≤ (𝑁‘(𝐴𝑀𝑦))) → 𝑥 = 𝑤))) | 
| 71 | 12, 65, 70 | sylanbrc 583 | 1
⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |