| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | minvec.f | . . 3
⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 2 |  | ssrab2 4079 | . . . . . 6
⊢ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌 | 
| 3 |  | minvec.y | . . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) | 
| 4 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑌 ∈ (LSubSp‘𝑈)) | 
| 5 |  | elpw2g 5332 | . . . . . . 7
⊢ (𝑌 ∈ (LSubSp‘𝑈) → ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌 ↔ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌)) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌 ↔ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌)) | 
| 7 | 2, 6 | mpbiri 258 | . . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌) | 
| 8 | 7 | fmpttd 7134 | . . . 4
⊢ (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}):ℝ+⟶𝒫
𝑌) | 
| 9 | 8 | frnd 6743 | . . 3
⊢ (𝜑 → ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ⊆ 𝒫 𝑌) | 
| 10 | 1, 9 | eqsstrid 4021 | . 2
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) | 
| 11 |  | 1rp 13039 | . . . . . 6
⊢ 1 ∈
ℝ+ | 
| 12 |  | eqid 2736 | . . . . . . 7
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 13 | 12, 7 | dmmptd 6712 | . . . . . 6
⊢ (𝜑 → dom (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ℝ+) | 
| 14 | 11, 13 | eleqtrrid 2847 | . . . . 5
⊢ (𝜑 → 1 ∈ dom (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) | 
| 15 | 14 | ne0d 4341 | . . . 4
⊢ (𝜑 → dom (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ≠ ∅) | 
| 16 |  | dm0rn0 5934 | . . . . . 6
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅ ↔ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅) | 
| 17 | 1 | eqeq1i 2741 | . . . . . 6
⊢ (𝐹 = ∅ ↔ ran (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅) | 
| 18 | 16, 17 | bitr4i 278 | . . . . 5
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅ ↔ 𝐹 = ∅) | 
| 19 | 18 | necon3bii 2992 | . . . 4
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ≠ ∅ ↔ 𝐹 ≠ ∅) | 
| 20 | 15, 19 | sylib 218 | . . 3
⊢ (𝜑 → 𝐹 ≠ ∅) | 
| 21 |  | minvec.x | . . . . . . . . . . . . . . . . . 18
⊢ 𝑋 = (Base‘𝑈) | 
| 22 |  | minvec.m | . . . . . . . . . . . . . . . . . 18
⊢  − =
(-g‘𝑈) | 
| 23 |  | minvec.n | . . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (norm‘𝑈) | 
| 24 |  | minvec.u | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) | 
| 25 |  | minvec.w | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) | 
| 26 |  | minvec.a | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 27 |  | minvec.j | . . . . . . . . . . . . . . . . . 18
⊢ 𝐽 = (TopOpen‘𝑈) | 
| 28 |  | minvec.r | . . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) | 
| 29 |  | minvec.s | . . . . . . . . . . . . . . . . . 18
⊢ 𝑆 = inf(𝑅, ℝ, < ) | 
| 30 | 21, 22, 23, 24, 3, 25, 26, 27, 28, 29 | minveclem4c 25460 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 31 | 30 | resqcld 14166 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) | 
| 32 |  | ltaddrp 13073 | . . . . . . . . . . . . . . . 16
⊢ (((𝑆↑2) ∈ ℝ ∧
𝑟 ∈
ℝ+) → (𝑆↑2) < ((𝑆↑2) + 𝑟)) | 
| 33 | 31, 32 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) < ((𝑆↑2) + 𝑟)) | 
| 34 | 31 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) ∈
ℝ) | 
| 35 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ) | 
| 37 | 34, 36 | readdcld 11291 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆↑2) + 𝑟) ∈ ℝ) | 
| 38 | 37 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆↑2) + 𝑟) ∈ ℂ) | 
| 39 | 38 | sqsqrtd 15479 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟))↑2) = ((𝑆↑2) + 𝑟)) | 
| 40 | 33, 39 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) <
((√‘((𝑆↑2)
+ 𝑟))↑2)) | 
| 41 | 21, 22, 23, 24, 3, 25, 26, 27, 28 | minveclem1 25459 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 42 | 41 | simp1d 1142 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ⊆ ℝ) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑅 ⊆
ℝ) | 
| 44 | 41 | simp2d 1143 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ≠ ∅) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑅 ≠ ∅) | 
| 46 |  | 0re 11264 | . . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ | 
| 47 | 41 | simp3d 1144 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) | 
| 48 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 0 → (𝑦 ≤ 𝑤 ↔ 0 ≤ 𝑤)) | 
| 49 | 48 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 0 → (∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | 
| 50 | 49 | rspcev 3621 | . . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) | 
| 51 | 46, 47, 50 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) | 
| 53 |  | infrecl 12251 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈
ℝ) | 
| 54 | 43, 45, 52, 53 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → inf(𝑅, ℝ, < ) ∈
ℝ) | 
| 55 | 29, 54 | eqeltrid 2844 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℝ) | 
| 56 |  | 0red 11265 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ∈
ℝ) | 
| 57 | 55 | sqge0d 14178 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(𝑆↑2)) | 
| 58 | 56, 34, 37, 57, 33 | lelttrd 11420 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 <
((𝑆↑2) + 𝑟)) | 
| 59 | 56, 37, 58 | ltled 11410 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
((𝑆↑2) + 𝑟)) | 
| 60 | 37, 59 | resqrtcld 15457 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(√‘((𝑆↑2)
+ 𝑟)) ∈
ℝ) | 
| 61 | 47 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑤 ∈ 𝑅 0 ≤ 𝑤) | 
| 62 |  | infregelb 12253 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) | 
| 63 | 43, 45, 52, 56, 62 | syl31anc 1374 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) | 
| 64 | 61, 63 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
inf(𝑅, ℝ, <
)) | 
| 65 | 64, 29 | breqtrrdi 5184 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
𝑆) | 
| 66 | 37, 59 | sqrtge0d 15460 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(√‘((𝑆↑2)
+ 𝑟))) | 
| 67 | 55, 60, 65, 66 | lt2sqd 14296 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (√‘((𝑆↑2) + 𝑟)) ↔ (𝑆↑2) < ((√‘((𝑆↑2) + 𝑟))↑2))) | 
| 68 | 40, 67 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 < (√‘((𝑆↑2) + 𝑟))) | 
| 69 | 55, 60 | ltnled 11409 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (√‘((𝑆↑2) + 𝑟)) ↔ ¬ (√‘((𝑆↑2) + 𝑟)) ≤ 𝑆)) | 
| 70 | 68, 69 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(√‘((𝑆↑2)
+ 𝑟)) ≤ 𝑆) | 
| 71 | 29 | breq2i 5150 | . . . . . . . . . . . . 13
⊢
((√‘((𝑆↑2) + 𝑟)) ≤ 𝑆 ↔ (√‘((𝑆↑2) + 𝑟)) ≤ inf(𝑅, ℝ, < )) | 
| 72 |  | infregelb 12253 | . . . . . . . . . . . . . . 15
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) ∧ (√‘((𝑆↑2) + 𝑟)) ∈ ℝ) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤)) | 
| 73 | 43, 45, 52, 60, 72 | syl31anc 1374 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤)) | 
| 74 | 28 | raleqi 3323 | . . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤) | 
| 75 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V | 
| 76 | 75 | rgenw 3064 | . . . . . . . . . . . . . . . 16
⊢
∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V | 
| 77 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) | 
| 78 |  | breq2 5146 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑁‘(𝐴 − 𝑦)) → ((√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 79 | 77, 78 | ralrnmptw 7113 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 80 | 76, 79 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 81 | 74, 80 | bitri 275 | . . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 82 | 73, 81 | bitrdi 287 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 83 | 71, 82 | bitrid 283 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ 𝑆 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 84 | 70, 83 | mtbid 324 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 85 |  | rexnal 3099 | . . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑌 ¬
(√‘((𝑆↑2)
+ 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ¬ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 86 | 84, 85 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) | 
| 87 | 60 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (√‘((𝑆↑2) + 𝑟)) ∈ ℝ) | 
| 88 |  | cphngp 25208 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) | 
| 89 | 24, 88 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ NrmGrp) | 
| 90 |  | ngpms 24614 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) | 
| 91 |  | minvec.d | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) | 
| 92 | 21, 91 | msmet 24468 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) | 
| 93 | 89, 90, 92 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 94 | 93 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) | 
| 95 | 26 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) | 
| 96 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) | 
| 97 | 21, 96 | lssss 20935 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) | 
| 98 | 4, 97 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑌 ⊆ 𝑋) | 
| 99 | 98 | sselda 3982 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) | 
| 100 |  | metcl 24343 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ) | 
| 101 | 94, 95, 99, 100 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) | 
| 102 | 66 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (√‘((𝑆↑2) + 𝑟))) | 
| 103 |  | metge0 24356 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦)) | 
| 104 | 94, 95, 99, 103 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦)) | 
| 105 | 87, 101, 102, 104 | le2sqd 14297 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝐴𝐷𝑦) ↔ ((√‘((𝑆↑2) + 𝑟))↑2) ≤ ((𝐴𝐷𝑦)↑2))) | 
| 106 | 91 | oveqi 7445 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴𝐷𝑦) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑦) | 
| 107 | 95, 99 | ovresd 7601 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑦) = (𝐴(dist‘𝑈)𝑦)) | 
| 108 | 106, 107 | eqtrid 2788 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) = (𝐴(dist‘𝑈)𝑦)) | 
| 109 | 89 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp) | 
| 110 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(dist‘𝑈) =
(dist‘𝑈) | 
| 111 | 23, 21, 22, 110 | ngpds 24618 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑦) = (𝑁‘(𝐴 − 𝑦))) | 
| 112 | 109, 95, 99, 111 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴(dist‘𝑈)𝑦) = (𝑁‘(𝐴 − 𝑦))) | 
| 113 | 108, 112 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) = (𝑁‘(𝐴 − 𝑦))) | 
| 114 | 113 | breq2d 5154 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝐴𝐷𝑦) ↔ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) | 
| 115 | 39 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟))↑2) = ((𝑆↑2) + 𝑟)) | 
| 116 | 115 | breq1d 5152 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (((√‘((𝑆↑2) + 𝑟))↑2) ≤ ((𝐴𝐷𝑦)↑2) ↔ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) | 
| 117 | 105, 114,
116 | 3bitr3d 309 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) | 
| 118 | 117 | notbid 318 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ¬ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) | 
| 119 | 37 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑟) ∈ ℝ) | 
| 120 | 101 | resqcld 14166 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦)↑2) ∈ ℝ) | 
| 121 | 119, 120 | letrid 11414 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2) ∨ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) | 
| 122 | 121 | ord 864 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) | 
| 123 | 118, 122 | sylbid 240 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) | 
| 124 | 123 | reximdva 3167 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) | 
| 125 | 86, 124 | mpd 15 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)) | 
| 126 |  | rabn0 4388 | . . . . . . . . 9
⊢ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)) | 
| 127 | 125, 126 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ≠ ∅) | 
| 128 | 127 | necomd 2995 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∅
≠ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 129 | 128 | neneqd 2944 | . . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 130 | 129 | nrexdv 3148 | . . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 131 | 1 | eleq2i 2832 | . . . . . 6
⊢ (∅
∈ 𝐹 ↔ ∅
∈ ran (𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) | 
| 132 |  | 0ex 5306 | . . . . . . 7
⊢ ∅
∈ V | 
| 133 | 12 | elrnmpt 5968 | . . . . . . 7
⊢ (∅
∈ V → (∅ ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ↔ ∃𝑟 ∈ ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) | 
| 134 | 132, 133 | ax-mp 5 | . . . . . 6
⊢ (∅
∈ ran (𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ↔ ∃𝑟 ∈ ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 135 | 131, 134 | bitri 275 | . . . . 5
⊢ (∅
∈ 𝐹 ↔
∃𝑟 ∈
ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 136 | 130, 135 | sylnibr 329 | . . . 4
⊢ (𝜑 → ¬ ∅ ∈ 𝐹) | 
| 137 |  | df-nel 3046 | . . . 4
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) | 
| 138 | 136, 137 | sylibr 234 | . . 3
⊢ (𝜑 → ∅ ∉ 𝐹) | 
| 139 | 55 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) | 
| 140 | 139 | resqcld 14166 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) | 
| 141 | 36 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑟 ∈ ℝ) | 
| 142 | 120, 140,
141 | lesubadd2d 11863 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) | 
| 143 | 142 | rabbidva 3442 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) | 
| 144 | 143 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) | 
| 145 | 144 | rneqd 5948 | . . . . . . . . 9
⊢ (𝜑 → ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) | 
| 146 | 1, 145 | eqtr4id 2795 | . . . . . . . 8
⊢ (𝜑 → 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) | 
| 147 | 146 | eleq2d 2826 | . . . . . . 7
⊢ (𝜑 → (𝑢 ∈ 𝐹 ↔ 𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}))) | 
| 148 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠)) | 
| 149 | 148 | rabbidv 3443 | . . . . . . . . . 10
⊢ (𝑟 = 𝑠 → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) | 
| 150 | 149 | cbvmptv 5254 | . . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑠 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) | 
| 151 | 150 | elrnmpt 5968 | . . . . . . . 8
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠})) | 
| 152 | 151 | elv 3484 | . . . . . . 7
⊢ (𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) | 
| 153 | 147, 152 | bitrdi 287 | . . . . . 6
⊢ (𝜑 → (𝑢 ∈ 𝐹 ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠})) | 
| 154 | 146 | eleq2d 2826 | . . . . . . 7
⊢ (𝜑 → (𝑣 ∈ 𝐹 ↔ 𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}))) | 
| 155 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)) | 
| 156 | 155 | rabbidv 3443 | . . . . . . . . . 10
⊢ (𝑟 = 𝑡 → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) | 
| 157 | 156 | cbvmptv 5254 | . . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑡 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) | 
| 158 | 157 | elrnmpt 5968 | . . . . . . . 8
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) | 
| 159 | 158 | elv 3484 | . . . . . . 7
⊢ (𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) | 
| 160 | 154, 159 | bitrdi 287 | . . . . . 6
⊢ (𝜑 → (𝑣 ∈ 𝐹 ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) | 
| 161 | 153, 160 | anbi12d 632 | . . . . 5
⊢ (𝜑 → ((𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹) ↔ (∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}))) | 
| 162 |  | reeanv 3228 | . . . . . 6
⊢
(∃𝑠 ∈
ℝ+ ∃𝑡 ∈ ℝ+ (𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) ↔ (∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) | 
| 163 | 93 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) | 
| 164 | 26 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) | 
| 165 | 3, 97 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ⊆ 𝑋) | 
| 166 | 165 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝑌 ⊆ 𝑋) | 
| 167 | 166 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) | 
| 168 | 163, 164,
167, 100 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) | 
| 169 | 168 | resqcld 14166 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦)↑2) ∈ ℝ) | 
| 170 | 31 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) | 
| 171 | 169, 170 | resubcld 11692 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ∈ ℝ) | 
| 172 |  | simplrl 776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑠 ∈ ℝ+) | 
| 173 | 172 | rpred 13078 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑠 ∈ ℝ) | 
| 174 |  | simplrr 777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑡 ∈ ℝ+) | 
| 175 | 174 | rpred 13078 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑡 ∈ ℝ) | 
| 176 |  | lemin 13235 | . . . . . . . . . . . 12
⊢
(((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) →
((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ↔ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡))) | 
| 177 | 171, 173,
175, 176 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ↔ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡))) | 
| 178 | 177 | rabbidva 3442 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)}) | 
| 179 |  | ifcl 4570 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℝ+
∧ 𝑡 ∈
ℝ+) → if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ∈
ℝ+) | 
| 180 | 3 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝑌 ∈
(LSubSp‘𝑈)) | 
| 181 |  | rabexg 5336 | . . . . . . . . . . . . 13
⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) | 
| 182 | 180, 181 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) | 
| 183 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) | 
| 184 |  | breq2 5146 | . . . . . . . . . . . . . 14
⊢ (𝑟 = if(𝑠 ≤ 𝑡, 𝑠, 𝑡) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡))) | 
| 185 | 184 | rabbidv 3443 | . . . . . . . . . . . . 13
⊢ (𝑟 = if(𝑠 ≤ 𝑡, 𝑠, 𝑡) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)}) | 
| 186 | 183, 185 | elrnmpt1s 5969 | . . . . . . . . . . . 12
⊢
((if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ∈ ℝ+ ∧ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) | 
| 187 | 179, 182,
186 | syl2an2 686 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) | 
| 188 | 146 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝐹 = ran (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) | 
| 189 | 187, 188 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ 𝐹) | 
| 190 | 178, 189 | eqeltrrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} ∈ 𝐹) | 
| 191 |  | ineq12 4214 | . . . . . . . . . . 11
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) = ({𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∩ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) | 
| 192 |  | inrab 4315 | . . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∩ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} | 
| 193 | 191, 192 | eqtrdi 2792 | . . . . . . . . . 10
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)}) | 
| 194 | 193 | eleq1d 2825 | . . . . . . . . 9
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → ((𝑢 ∩ 𝑣) ∈ 𝐹 ↔ {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} ∈ 𝐹)) | 
| 195 | 190, 194 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) ∈ 𝐹)) | 
| 196 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑢 ∈ V | 
| 197 | 196 | inex1 5316 | . . . . . . . . . 10
⊢ (𝑢 ∩ 𝑣) ∈ V | 
| 198 | 197 | pwid 4621 | . . . . . . . . 9
⊢ (𝑢 ∩ 𝑣) ∈ 𝒫 (𝑢 ∩ 𝑣) | 
| 199 |  | inelcm 4464 | . . . . . . . . 9
⊢ (((𝑢 ∩ 𝑣) ∈ 𝐹 ∧ (𝑢 ∩ 𝑣) ∈ 𝒫 (𝑢 ∩ 𝑣)) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) | 
| 200 | 198, 199 | mpan2 691 | . . . . . . . 8
⊢ ((𝑢 ∩ 𝑣) ∈ 𝐹 → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) | 
| 201 | 195, 200 | syl6 35 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) | 
| 202 | 201 | rexlimdvva 3212 | . . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ ℝ+ ∃𝑡 ∈ ℝ+
(𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) | 
| 203 | 162, 202 | biimtrrid 243 | . . . . 5
⊢ (𝜑 → ((∃𝑠 ∈ ℝ+
𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) | 
| 204 | 161, 203 | sylbid 240 | . . . 4
⊢ (𝜑 → ((𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) | 
| 205 | 204 | ralrimivv 3199 | . . 3
⊢ (𝜑 → ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) | 
| 206 | 20, 138, 205 | 3jca 1128 | . 2
⊢ (𝜑 → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) | 
| 207 |  | isfbas 23838 | . . 3
⊢ (𝑌 ∈ (LSubSp‘𝑈) → (𝐹 ∈ (fBas‘𝑌) ↔ (𝐹 ⊆ 𝒫 𝑌 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)))) | 
| 208 | 3, 207 | syl 17 | . 2
⊢ (𝜑 → (𝐹 ∈ (fBas‘𝑌) ↔ (𝐹 ⊆ 𝒫 𝑌 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)))) | 
| 209 | 10, 206, 208 | mpbir2and 713 | 1
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |