| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | minvec.d | . . . . . . . 8
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) | 
| 2 | 1 | oveqi 7444 | . . . . . . 7
⊢ (𝐴𝐷𝑥) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑥) | 
| 3 |  | minvec.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 4 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐴 ∈ 𝑋) | 
| 5 |  | minvec.y | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) | 
| 6 |  | minvec.x | . . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝑈) | 
| 7 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) | 
| 8 | 6, 7 | lssss 20934 | . . . . . . . . . 10
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) | 
| 9 | 5, 8 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ⊆ 𝑋) | 
| 10 | 9 | sselda 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) | 
| 11 | 4, 10 | ovresd 7600 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑥) = (𝐴(dist‘𝑈)𝑥)) | 
| 12 | 2, 11 | eqtrid 2789 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴𝐷𝑥) = (𝐴(dist‘𝑈)𝑥)) | 
| 13 |  | minvec.u | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) | 
| 14 |  | cphngp 25207 | . . . . . . . . 9
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) | 
| 15 | 13, 14 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ NrmGrp) | 
| 16 | 15 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑈 ∈ NrmGrp) | 
| 17 |  | minvec.n | . . . . . . . 8
⊢ 𝑁 = (norm‘𝑈) | 
| 18 |  | minvec.m | . . . . . . . 8
⊢  − =
(-g‘𝑈) | 
| 19 |  | eqid 2737 | . . . . . . . 8
⊢
(dist‘𝑈) =
(dist‘𝑈) | 
| 20 | 17, 6, 18, 19 | ngpds 24617 | . . . . . . 7
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑥) = (𝑁‘(𝐴 − 𝑥))) | 
| 21 | 16, 4, 10, 20 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴(dist‘𝑈)𝑥) = (𝑁‘(𝐴 − 𝑥))) | 
| 22 | 12, 21 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴𝐷𝑥) = (𝑁‘(𝐴 − 𝑥))) | 
| 23 | 22 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐴𝐷𝑥)↑2) = ((𝑁‘(𝐴 − 𝑥))↑2)) | 
| 24 |  | minvec.s | . . . . . . . 8
⊢ 𝑆 = inf(𝑅, ℝ, < ) | 
| 25 |  | minvec.w | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) | 
| 26 |  | minvec.j | . . . . . . . . . . . 12
⊢ 𝐽 = (TopOpen‘𝑈) | 
| 27 |  | minvec.r | . . . . . . . . . . . 12
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) | 
| 28 | 6, 18, 17, 13, 5, 25, 3, 26, 27 | minveclem1 25458 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 29 | 28 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 30 | 29 | simp1d 1143 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑅 ⊆ ℝ) | 
| 31 | 29 | simp2d 1144 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑅 ≠ ∅) | 
| 32 |  | 0red 11264 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ∈ ℝ) | 
| 33 | 29 | simp3d 1145 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) | 
| 34 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) | 
| 35 | 34 | ralbidv 3178 | . . . . . . . . . . 11
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 36 | 35 | rspcev 3622 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) | 
| 37 | 32, 33, 36 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) | 
| 38 |  | infrecl 12250 | . . . . . . . . 9
⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈
ℝ) | 
| 39 | 30, 31, 37, 38 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → inf(𝑅, ℝ, < ) ∈
ℝ) | 
| 40 | 24, 39 | eqeltrid 2845 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ ℝ) | 
| 41 | 40 | resqcld 14165 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) | 
| 42 | 41 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆↑2) ∈ ℂ) | 
| 43 | 42 | addridd 11461 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆↑2) + 0) = (𝑆↑2)) | 
| 44 | 23, 43 | breq12d 5156 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ((𝑁‘(𝐴 − 𝑥))↑2) ≤ (𝑆↑2))) | 
| 45 |  | cphlmod 25208 | . . . . . . . 8
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
LMod) | 
| 46 | 13, 45 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LMod) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑈 ∈ LMod) | 
| 48 | 6, 18 | lmodvsubcl 20905 | . . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐴 − 𝑥) ∈ 𝑋) | 
| 49 | 47, 4, 10, 48 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴 − 𝑥) ∈ 𝑋) | 
| 50 | 6, 17 | nmcl 24629 | . . . . 5
⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑥) ∈ 𝑋) → (𝑁‘(𝐴 − 𝑥)) ∈ ℝ) | 
| 51 | 16, 49, 50 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑁‘(𝐴 − 𝑥)) ∈ ℝ) | 
| 52 | 6, 17 | nmge0 24630 | . . . . 5
⊢ ((𝑈 ∈ NrmGrp ∧ (𝐴 − 𝑥) ∈ 𝑋) → 0 ≤ (𝑁‘(𝐴 − 𝑥))) | 
| 53 | 16, 49, 52 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ (𝑁‘(𝐴 − 𝑥))) | 
| 54 |  | infregelb 12252 | . . . . . . 7
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) | 
| 55 | 30, 31, 37, 32, 54 | syl31anc 1375 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 56 | 33, 55 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ inf(𝑅, ℝ, < )) | 
| 57 | 56, 24 | breqtrrdi 5185 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ 𝑆) | 
| 58 | 51, 40, 53, 57 | le2sqd 14296 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴 − 𝑥)) ≤ 𝑆 ↔ ((𝑁‘(𝐴 − 𝑥))↑2) ≤ (𝑆↑2))) | 
| 59 | 24 | breq2i 5151 | . . . 4
⊢ ((𝑁‘(𝐴 − 𝑥)) ≤ 𝑆 ↔ (𝑁‘(𝐴 − 𝑥)) ≤ inf(𝑅, ℝ, < )) | 
| 60 |  | infregelb 12252 | . . . . 5
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ (𝑁‘(𝐴 − 𝑥)) ∈ ℝ) → ((𝑁‘(𝐴 − 𝑥)) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤)) | 
| 61 | 30, 31, 37, 51, 60 | syl31anc 1375 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴 − 𝑥)) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤)) | 
| 62 | 59, 61 | bitrid 283 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴 − 𝑥)) ≤ 𝑆 ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤)) | 
| 63 | 44, 58, 62 | 3bitr2d 307 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤)) | 
| 64 | 27 | raleqi 3324 | . . 3
⊢
(∀𝑤 ∈
𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(𝑁‘(𝐴 − 𝑥)) ≤ 𝑤) | 
| 65 |  | fvex 6919 | . . . . 5
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V | 
| 66 | 65 | rgenw 3065 | . . . 4
⊢
∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V | 
| 67 |  | eqid 2737 | . . . . 5
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) | 
| 68 |  | breq2 5147 | . . . . 5
⊢ (𝑤 = (𝑁‘(𝐴 − 𝑦)) → ((𝑁‘(𝐴 − 𝑥)) ≤ 𝑤 ↔ (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 69 | 67, 68 | ralrnmptw 7114 | . . . 4
⊢
(∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(𝑁‘(𝐴 − 𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 70 | 66, 69 | ax-mp 5 | . . 3
⊢
(∀𝑤 ∈
ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(𝑁‘(𝐴 − 𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 71 | 64, 70 | bitri 275 | . 2
⊢
(∀𝑤 ∈
𝑅 (𝑁‘(𝐴 − 𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 72 | 63, 71 | bitrdi 287 | 1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) |