Step | Hyp | Ref
| Expression |
1 | | minvec.p |
. 2
⊢ 𝑃 = ∪
(𝐽 fLim (𝑋filGen𝐹)) |
2 | | ovex 6577 |
. . . . 5
⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V |
3 | 2 | uniex 6851 |
. . . 4
⊢ ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ V |
4 | 3 | snid 4155 |
. . 3
⊢ ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽
fLim (𝑋filGen𝐹))} |
5 | | minvec.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) |
6 | | cphngp 22781 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
7 | | ngpxms 22215 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈
∞MetSp) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ ∞MetSp) |
9 | | minvec.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (TopOpen‘𝑈) |
10 | | minvec.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝑈) |
11 | | minvec.d |
. . . . . . . . . . . 12
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) |
12 | 9, 10, 11 | xmstopn 22066 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐽 = (MetOpen‘𝐷)) |
13 | 8, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |
14 | 13 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ↾t 𝑌) = ((MetOpen‘𝐷) ↾t 𝑌)) |
15 | 10, 11 | xmsxmet 22071 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐷 ∈
(∞Met‘𝑋)) |
16 | 8, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
17 | | minvec.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) |
18 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
19 | 10, 18 | lssss 18758 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
20 | 17, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
21 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) |
22 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
23 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) |
24 | 21, 22, 23 | metrest 22139 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
25 | 16, 20, 24 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((MetOpen‘𝐷) ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
26 | 14, 25 | eqtr2d 2645 |
. . . . . . . 8
⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (𝐽 ↾t 𝑌)) |
27 | | minvec.m |
. . . . . . . . . . . 12
⊢ − =
(-g‘𝑈) |
28 | | minvec.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (norm‘𝑈) |
29 | | minvec.w |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) |
30 | | minvec.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
31 | | minvec.r |
. . . . . . . . . . . 12
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
32 | | minvec.s |
. . . . . . . . . . . 12
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
33 | | minvec.f |
. . . . . . . . . . . 12
⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
34 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33 | minveclem3b 23007 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |
35 | | fgcl 21492 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌)) |
37 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝑈)
∈ V |
38 | 10, 37 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝑋 ∈ V |
39 | 38 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
40 | | trfg 21505 |
. . . . . . . . . 10
⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = (𝑌filGen𝐹)) |
41 | 36, 20, 39, 40 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = (𝑌filGen𝐹)) |
42 | | fgabs 21493 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) |
43 | 34, 20, 42 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) |
44 | 43 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = ((𝑋filGen𝐹) ↾t 𝑌)) |
45 | 41, 44 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾t 𝑌)) |
46 | 26, 45 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌))) |
47 | | xmstps 22068 |
. . . . . . . . . 10
⊢ (𝑈 ∈ ∞MetSp →
𝑈 ∈
TopSp) |
48 | 8, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ TopSp) |
49 | 10, 9 | istps 20551 |
. . . . . . . . 9
⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋)) |
50 | 48, 49 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
51 | | fbsspw 21446 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌) |
52 | 34, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
53 | | sspwb 4844 |
. . . . . . . . . . . 12
⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋) |
54 | 20, 53 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
55 | 52, 54 | sstrd 3578 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋) |
56 | | fbasweak 21479 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋)) |
57 | 34, 55, 39, 56 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋)) |
58 | | fgcl 21492 |
. . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
59 | 57, 58 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
60 | | filfbas 21462 |
. . . . . . . . . . . . 13
⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌)) |
61 | 34, 35, 60 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌)) |
62 | | fbsspw 21446 |
. . . . . . . . . . . . . 14
⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌) |
64 | 63, 54 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋) |
65 | | fbasweak 21479 |
. . . . . . . . . . . 12
⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋)) |
66 | 61, 64, 39, 65 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋)) |
67 | | ssfg 21486 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹))) |
68 | 66, 67 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹))) |
69 | 68, 43 | sseqtrd 3604 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹)) |
70 | | filtop 21469 |
. . . . . . . . . 10
⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹)) |
71 | 36, 70 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹)) |
72 | 69, 71 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹)) |
73 | | flimrest 21597 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
74 | 50, 59, 72, 73 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
75 | 46, 74 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
76 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11 | minveclem3a 23006 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) |
77 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33 | minveclem3 23008 |
. . . . . . 7
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) |
78 | 23 | cmetcvg 22891 |
. . . . . . 7
⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅) |
79 | 76, 77, 78 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅) |
80 | 75, 79 | eqnetrrd 2850 |
. . . . 5
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) |
81 | 80 | neneqd 2787 |
. . . 4
⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅) |
82 | | inss1 3795 |
. . . . . . 7
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) |
83 | 22 | methaus 22135 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus) |
84 | 15, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ∞MetSp →
(MetOpen‘𝐷) ∈
Haus) |
85 | 12, 84 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐽 ∈
Haus) |
86 | | hausflimi 21594 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Haus →
∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
87 | 8, 85, 86 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
88 | | ssn0 3928 |
. . . . . . . . . . . 12
⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅) |
89 | 82, 80, 88 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅) |
90 | | n0moeu 3893 |
. . . . . . . . . . 11
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≠ ∅ → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))) |
92 | 87, 91 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
93 | | euen1b 7913 |
. . . . . . . . 9
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1𝑜 ↔
∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
94 | 92, 93 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈
1𝑜) |
95 | | en1b 7910 |
. . . . . . . 8
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1𝑜 ↔
(𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
96 | 94, 95 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
97 | 82, 96 | syl5sseq 3616 |
. . . . . 6
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪
(𝐽 fLim (𝑋filGen𝐹))}) |
98 | | sssn 4298 |
. . . . . 6
⊢ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪
(𝐽 fLim (𝑋filGen𝐹))} ↔ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
99 | 97, 98 | sylib 207 |
. . . . 5
⊢ (𝜑 → (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
100 | 99 | ord 391 |
. . . 4
⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
101 | 81, 100 | mpd 15 |
. . 3
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
102 | 4, 101 | syl5eleqr 2695 |
. 2
⊢ (𝜑 → ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
103 | 1, 102 | syl5eqel 2692 |
1
⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |