Step | Hyp | Ref
| Expression |
1 | | minvec.f |
. . 3
⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
2 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌 |
3 | | minvec.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑌 ∈ (LSubSp‘𝑈)) |
5 | | elpw2g 4827 |
. . . . . . 7
⊢ (𝑌 ∈ (LSubSp‘𝑈) → ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌 ↔ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌)) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌 ↔ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ⊆ 𝑌)) |
7 | 2, 6 | mpbiri 248 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ∈ 𝒫 𝑌) |
8 | | eqid 2622 |
. . . . 5
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
9 | 7, 8 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}):ℝ+⟶𝒫
𝑌) |
10 | | frn 6053 |
. . . 4
⊢ ((𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}):ℝ+⟶𝒫
𝑌 → ran (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ⊆ 𝒫 𝑌) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ⊆ 𝒫 𝑌) |
12 | 1, 11 | syl5eqss 3649 |
. 2
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
13 | | 1rp 11836 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
14 | 8, 7 | dmmptd 6024 |
. . . . . 6
⊢ (𝜑 → dom (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ℝ+) |
15 | 13, 14 | syl5eleqr 2708 |
. . . . 5
⊢ (𝜑 → 1 ∈ dom (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
16 | | ne0i 3921 |
. . . . 5
⊢ (1 ∈
dom (𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) → dom (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ≠ ∅) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ≠ ∅) |
18 | | dm0rn0 5342 |
. . . . . 6
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅ ↔ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅) |
19 | 1 | eqeq1i 2627 |
. . . . . 6
⊢ (𝐹 = ∅ ↔ ran (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅) |
20 | 18, 19 | bitr4i 267 |
. . . . 5
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) = ∅ ↔ 𝐹 = ∅) |
21 | 20 | necon3bii 2846 |
. . . 4
⊢ (dom
(𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ≠ ∅ ↔ 𝐹 ≠ ∅) |
22 | 17, 21 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐹 ≠ ∅) |
23 | | minvec.x |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 = (Base‘𝑈) |
24 | | minvec.m |
. . . . . . . . . . . . . . . . . 18
⊢ − =
(-g‘𝑈) |
25 | | minvec.n |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (norm‘𝑈) |
26 | | minvec.u |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) |
27 | | minvec.w |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) |
28 | | minvec.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
29 | | minvec.j |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐽 = (TopOpen‘𝑈) |
30 | | minvec.r |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
31 | | minvec.s |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
32 | 23, 24, 25, 26, 3, 27, 28, 29, 30, 31 | minveclem4c 23196 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 ∈ ℝ) |
33 | 32 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆↑2) ∈ ℝ) |
34 | | ltaddrp 11867 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆↑2) ∈ ℝ ∧
𝑟 ∈
ℝ+) → (𝑆↑2) < ((𝑆↑2) + 𝑟)) |
35 | 33, 34 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) < ((𝑆↑2) + 𝑟)) |
36 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) ∈
ℝ) |
37 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ) |
39 | 36, 38 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆↑2) + 𝑟) ∈ ℝ) |
40 | 39 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑆↑2) + 𝑟) ∈ ℂ) |
41 | 40 | sqsqrtd 14178 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟))↑2) = ((𝑆↑2) + 𝑟)) |
42 | 35, 41 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆↑2) <
((√‘((𝑆↑2)
+ 𝑟))↑2)) |
43 | 23, 24, 25, 26, 3, 27, 28, 29, 30 | minveclem1 23195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
44 | 43 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ⊆ ℝ) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑅 ⊆
ℝ) |
46 | 43 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑅 ≠ ∅) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑅 ≠ ∅) |
48 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
49 | 43 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
50 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 0 → (𝑦 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
51 | 50 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 0 → (∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
52 | 51 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) |
53 | 48, 49, 52 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) |
55 | | infrecl 11005 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈
ℝ) |
56 | 45, 47, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → inf(𝑅, ℝ, < ) ∈
ℝ) |
57 | 31, 56 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 ∈
ℝ) |
58 | | 0red 10041 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ∈
ℝ) |
59 | 57 | sqge0d 13036 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(𝑆↑2)) |
60 | 58, 36, 39, 59, 35 | lelttrd 10195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 <
((𝑆↑2) + 𝑟)) |
61 | 58, 39, 60 | ltled 10185 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
((𝑆↑2) + 𝑟)) |
62 | 39, 61 | resqrtcld 14156 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(√‘((𝑆↑2)
+ 𝑟)) ∈
ℝ) |
63 | 49 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
64 | | infregelb 11007 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
65 | 45, 47, 54, 58, 64 | syl31anc 1329 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
66 | 63, 65 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
inf(𝑅, ℝ, <
)) |
67 | 66, 31 | syl6breqr 4695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
𝑆) |
68 | 39, 61 | sqrtge0d 14159 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(√‘((𝑆↑2)
+ 𝑟))) |
69 | 57, 62, 67, 68 | lt2sqd 13043 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (√‘((𝑆↑2) + 𝑟)) ↔ (𝑆↑2) < ((√‘((𝑆↑2) + 𝑟))↑2))) |
70 | 42, 69 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑆 < (√‘((𝑆↑2) + 𝑟))) |
71 | 57, 62 | ltnled 10184 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑆 < (√‘((𝑆↑2) + 𝑟)) ↔ ¬ (√‘((𝑆↑2) + 𝑟)) ≤ 𝑆)) |
72 | 70, 71 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
(√‘((𝑆↑2)
+ 𝑟)) ≤ 𝑆) |
73 | 31 | breq2i 4661 |
. . . . . . . . . . . . 13
⊢
((√‘((𝑆↑2) + 𝑟)) ≤ 𝑆 ↔ (√‘((𝑆↑2) + 𝑟)) ≤ inf(𝑅, ℝ, < )) |
74 | | infregelb 11007 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑦 ≤ 𝑤) ∧ (√‘((𝑆↑2) + 𝑟)) ∈ ℝ) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤)) |
75 | 45, 47, 54, 62, 74 | syl31anc 1329 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤)) |
76 | 30 | raleqi 3142 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤) |
77 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁‘(𝐴 − 𝑦)) ∈ V |
78 | 77 | rgenw 2924 |
. . . . . . . . . . . . . . . 16
⊢
∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V |
79 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
80 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝑁‘(𝐴 − 𝑦)) → ((√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
81 | 79, 80 | ralrnmpt 6368 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝑌 (𝑁‘(𝐴 − 𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
82 | 78, 81 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))(√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) |
83 | 76, 82 | bitri 264 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + 𝑟)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) |
84 | 75, 83 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
85 | 73, 84 | syl5bb 272 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((√‘((𝑆↑2)
+ 𝑟)) ≤ 𝑆 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
86 | 72, 85 | mtbid 314 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) |
87 | | rexnal 2995 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑌 ¬
(√‘((𝑆↑2)
+ 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ¬ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) |
88 | 86, 87 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦))) |
89 | 62 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (√‘((𝑆↑2) + 𝑟)) ∈ ℝ) |
90 | | cphngp 22973 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
91 | 26, 90 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈ NrmGrp) |
92 | | ngpms 22404 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ MetSp) |
93 | | minvec.d |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) |
94 | 23, 93 | msmet 22262 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
95 | 91, 92, 94 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
96 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) |
97 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
98 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
99 | 23, 98 | lssss 18937 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
100 | 4, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑌 ⊆ 𝑋) |
101 | 100 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
102 | | metcl 22137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) ∈ ℝ) |
103 | 96, 97, 101, 102 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) |
104 | 68 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (√‘((𝑆↑2) + 𝑟))) |
105 | | metge0 22150 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝑦)) |
106 | 96, 97, 101, 105 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝐴𝐷𝑦)) |
107 | 89, 103, 104, 106 | le2sqd 13044 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝐴𝐷𝑦) ↔ ((√‘((𝑆↑2) + 𝑟))↑2) ≤ ((𝐴𝐷𝑦)↑2))) |
108 | 93 | oveqi 6663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴𝐷𝑦) = (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑦) |
109 | 97, 101 | ovresd 6801 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴((dist‘𝑈) ↾ (𝑋 × 𝑋))𝑦) = (𝐴(dist‘𝑈)𝑦)) |
110 | 108, 109 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) = (𝐴(dist‘𝑈)𝑦)) |
111 | 91 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmGrp) |
112 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(dist‘𝑈) =
(dist‘𝑈) |
113 | 25, 23, 24, 112 | ngpds 22408 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴(dist‘𝑈)𝑦) = (𝑁‘(𝐴 − 𝑦))) |
114 | 111, 97, 101, 113 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴(dist‘𝑈)𝑦) = (𝑁‘(𝐴 − 𝑦))) |
115 | 110, 114 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) = (𝑁‘(𝐴 − 𝑦))) |
116 | 115 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝐴𝐷𝑦) ↔ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)))) |
117 | 41 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟))↑2) = ((𝑆↑2) + 𝑟)) |
118 | 117 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (((√‘((𝑆↑2) + 𝑟))↑2) ≤ ((𝐴𝐷𝑦)↑2) ↔ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) |
119 | 107, 116,
118 | 3bitr3d 298 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) |
120 | 119 | notbid 308 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ ¬ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2))) |
121 | 39 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + 𝑟) ∈ ℝ) |
122 | 103 | resqcld 13035 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦)↑2) ∈ ℝ) |
123 | 121, 122 | letrid 10189 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2) ∨ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) |
124 | 123 | ord 392 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ ((𝑆↑2) + 𝑟) ≤ ((𝐴𝐷𝑦)↑2) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) |
125 | 120, 124 | sylbid 230 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) |
126 | 125 | reximdva 3017 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + 𝑟)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) |
127 | 88, 126 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)) |
128 | | rabn0 3958 |
. . . . . . . . 9
⊢ ({𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ≠ ∅ ↔ ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)) |
129 | 127, 128 | sylibr 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)} ≠ ∅) |
130 | 129 | necomd 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∅
≠ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
131 | 130 | neneqd 2799 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ¬
∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
132 | 131 | nrexdv 3001 |
. . . . 5
⊢ (𝜑 → ¬ ∃𝑟 ∈ ℝ+
∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
133 | 1 | eleq2i 2693 |
. . . . . 6
⊢ (∅
∈ 𝐹 ↔ ∅
∈ ran (𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
134 | | 0ex 4790 |
. . . . . . 7
⊢ ∅
∈ V |
135 | 8 | elrnmpt 5372 |
. . . . . . 7
⊢ (∅
∈ V → (∅ ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ↔ ∃𝑟 ∈ ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
136 | 134, 135 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ ran (𝑟 ∈
ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ↔ ∃𝑟 ∈ ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
137 | 133, 136 | bitri 264 |
. . . . 5
⊢ (∅
∈ 𝐹 ↔
∃𝑟 ∈
ℝ+ ∅ = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
138 | 132, 137 | sylnibr 319 |
. . . 4
⊢ (𝜑 → ¬ ∅ ∈ 𝐹) |
139 | | df-nel 2898 |
. . . 4
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
140 | 138, 139 | sylibr 224 |
. . 3
⊢ (𝜑 → ∅ ∉ 𝐹) |
141 | 57 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑆 ∈ ℝ) |
142 | 141 | resqcld 13035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
143 | 38 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → 𝑟 ∈ ℝ) |
144 | 122, 142,
143 | lesubadd2d 10626 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟))) |
145 | 144 | rabbidva 3188 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
146 | 145 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
147 | 146 | rneqd 5353 |
. . . . . . . . 9
⊢ (𝜑 → ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})) |
148 | 147, 1 | syl6reqr 2675 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) |
149 | 148 | eleq2d 2687 |
. . . . . . 7
⊢ (𝜑 → (𝑢 ∈ 𝐹 ↔ 𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}))) |
150 | | vex 3203 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
151 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑠 → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠)) |
152 | 151 | rabbidv 3189 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑠 → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) |
153 | 152 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑠 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) |
154 | 153 | elrnmpt 5372 |
. . . . . . . 8
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠})) |
155 | 150, 154 | ax-mp 5 |
. . . . . . 7
⊢ (𝑢 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠}) |
156 | 149, 155 | syl6bb 276 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ 𝐹 ↔ ∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠})) |
157 | 148 | eleq2d 2687 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ 𝐹 ↔ 𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}))) |
158 | | vex 3203 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
159 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)) |
160 | 159 | rabbidv 3189 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑡 → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) |
161 | 160 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑡 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) |
162 | 161 | elrnmpt 5372 |
. . . . . . . 8
⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) |
163 | 158, 162 | ax-mp 5 |
. . . . . . 7
⊢ (𝑣 ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) |
164 | 157, 163 | syl6bb 276 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ 𝐹 ↔ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) |
165 | 156, 164 | anbi12d 747 |
. . . . 5
⊢ (𝜑 → ((𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹) ↔ (∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}))) |
166 | | reeanv 3107 |
. . . . . 6
⊢
(∃𝑠 ∈
ℝ+ ∃𝑡 ∈ ℝ+ (𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) ↔ (∃𝑠 ∈ ℝ+ 𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) |
167 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝐷 ∈ (Met‘𝑋)) |
168 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
169 | 3, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝑌 ⊆ 𝑋) |
171 | 170 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
172 | 167, 168,
171, 102 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) ∈ ℝ) |
173 | 172 | resqcld 13035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦)↑2) ∈ ℝ) |
174 | 33 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
175 | 173, 174 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ∈ ℝ) |
176 | | simplrl 800 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑠 ∈ ℝ+) |
177 | 176 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑠 ∈ ℝ) |
178 | | simplrr 801 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑡 ∈ ℝ+) |
179 | 178 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → 𝑡 ∈ ℝ) |
180 | | lemin 12023 |
. . . . . . . . . . . 12
⊢
(((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) →
((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ↔ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡))) |
181 | 175, 177,
179, 180 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
∧ 𝑦 ∈ 𝑌) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ↔ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡))) |
182 | 181 | rabbidva 3188 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)}) |
183 | | ifcl 4130 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈ ℝ+
∧ 𝑡 ∈
ℝ+) → if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ∈
ℝ+) |
184 | 183 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ∈
ℝ+) |
185 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝑌 ∈
(LSubSp‘𝑈)) |
186 | | rabexg 4812 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (LSubSp‘𝑈) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) |
188 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) = (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟}) |
189 | | breq2 4657 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = if(𝑠 ≤ 𝑡, 𝑠, 𝑡) → ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟 ↔ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡))) |
190 | 189 | rabbidv 3189 |
. . . . . . . . . . . . 13
⊢ (𝑟 = if(𝑠 ≤ 𝑡, 𝑠, 𝑡) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟} = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)}) |
191 | 188, 190 | elrnmpt1s 5373 |
. . . . . . . . . . . 12
⊢
((if(𝑠 ≤ 𝑡, 𝑠, 𝑡) ∈ ℝ+ ∧ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ V) → {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) |
192 | 184, 187,
191 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) |
193 | 148 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ 𝐹 = ran (𝑟 ∈ ℝ+
↦ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑟})) |
194 | 192, 193 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ if(𝑠 ≤ 𝑡, 𝑠, 𝑡)} ∈ 𝐹) |
195 | 182, 194 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} ∈ 𝐹) |
196 | | ineq12 3809 |
. . . . . . . . . . 11
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) = ({𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∩ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡})) |
197 | | inrab 3899 |
. . . . . . . . . . 11
⊢ ({𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∩ {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} |
198 | 196, 197 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) = {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)}) |
199 | 198 | eleq1d 2686 |
. . . . . . . . 9
⊢ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → ((𝑢 ∩ 𝑣) ∈ 𝐹 ↔ {𝑦 ∈ 𝑌 ∣ ((((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠 ∧ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡)} ∈ 𝐹)) |
200 | 195, 199 | syl5ibrcom 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝑢 ∩ 𝑣) ∈ 𝐹)) |
201 | 150 | inex1 4799 |
. . . . . . . . . 10
⊢ (𝑢 ∩ 𝑣) ∈ V |
202 | 201 | pwid 4174 |
. . . . . . . . 9
⊢ (𝑢 ∩ 𝑣) ∈ 𝒫 (𝑢 ∩ 𝑣) |
203 | | inelcm 4032 |
. . . . . . . . 9
⊢ (((𝑢 ∩ 𝑣) ∈ 𝐹 ∧ (𝑢 ∩ 𝑣) ∈ 𝒫 (𝑢 ∩ 𝑣)) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) |
204 | 202, 203 | mpan2 707 |
. . . . . . . 8
⊢ ((𝑢 ∩ 𝑣) ∈ 𝐹 → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) |
205 | 200, 204 | syl6 35 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+))
→ ((𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) |
206 | 205 | rexlimdvva 3038 |
. . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ ℝ+ ∃𝑡 ∈ ℝ+
(𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) |
207 | 166, 206 | syl5bir 233 |
. . . . 5
⊢ (𝜑 → ((∃𝑠 ∈ ℝ+
𝑢 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑠} ∧ ∃𝑡 ∈ ℝ+ 𝑣 = {𝑦 ∈ 𝑌 ∣ (((𝐴𝐷𝑦)↑2) − (𝑆↑2)) ≤ 𝑡}) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) |
208 | 165, 207 | sylbid 230 |
. . . 4
⊢ (𝜑 → ((𝑢 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹) → (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) |
209 | 208 | ralrimivv 2970 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅) |
210 | 22, 140, 209 | 3jca 1242 |
. 2
⊢ (𝜑 → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)) |
211 | | isfbas 21633 |
. . 3
⊢ (𝑌 ∈ (LSubSp‘𝑈) → (𝐹 ∈ (fBas‘𝑌) ↔ (𝐹 ⊆ 𝒫 𝑌 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)))) |
212 | 3, 211 | syl 17 |
. 2
⊢ (𝜑 → (𝐹 ∈ (fBas‘𝑌) ↔ (𝐹 ⊆ 𝒫 𝑌 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑢 ∈ 𝐹 ∀𝑣 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑢 ∩ 𝑣)) ≠ ∅)))) |
213 | 12, 210, 212 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |