Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . 4
β’ (π β π β
CPreHilOLD) |
2 | | phnv 29798 |
. . . 4
β’ (π β CPreHilOLD
β π β
NrmCVec) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π β NrmCVec) |
4 | | minveco.w |
. . . . 5
β’ (π β π β ((SubSpβπ) β© CBan)) |
5 | | elin 3927 |
. . . . 5
β’ (π β ((SubSpβπ) β© CBan) β (π β (SubSpβπ) β§ π β CBan)) |
6 | 4, 5 | sylib 217 |
. . . 4
β’ (π β (π β (SubSpβπ) β§ π β CBan)) |
7 | 6 | simpld 496 |
. . 3
β’ (π β π β (SubSpβπ)) |
8 | | minveco.x |
. . . 4
β’ π = (BaseSetβπ) |
9 | | minveco.y |
. . . 4
β’ π = (BaseSetβπ) |
10 | | eqid 2733 |
. . . 4
β’
(SubSpβπ) =
(SubSpβπ) |
11 | 8, 9, 10 | sspba 29711 |
. . 3
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
12 | 3, 7, 11 | syl2anc 585 |
. 2
β’ (π β π β π) |
13 | | minveco.d |
. . . . . . . 8
β’ π· = (IndMetβπ) |
14 | 8, 13 | imsxmet 29676 |
. . . . . . 7
β’ (π β NrmCVec β π· β (βMetβπ)) |
15 | 3, 14 | syl 17 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
16 | | minveco.j |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
17 | 16 | methaus 23892 |
. . . . . 6
β’ (π· β (βMetβπ) β π½ β Haus) |
18 | 15, 17 | syl 17 |
. . . . 5
β’ (π β π½ β Haus) |
19 | | lmfun 22748 |
. . . . 5
β’ (π½ β Haus β Fun
(βπ‘βπ½)) |
20 | 18, 19 | syl 17 |
. . . 4
β’ (π β Fun
(βπ‘βπ½)) |
21 | | minveco.m |
. . . . . 6
β’ π = ( βπ£
βπ) |
22 | | minveco.n |
. . . . . 6
β’ π =
(normCVβπ) |
23 | | minveco.a |
. . . . . 6
β’ (π β π΄ β π) |
24 | | minveco.r |
. . . . . 6
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
25 | | minveco.s |
. . . . . 6
β’ π = inf(π
, β, < ) |
26 | | minveco.f |
. . . . . 6
β’ (π β πΉ:ββΆπ) |
27 | | minveco.1 |
. . . . . 6
β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) |
28 | 8, 21, 22, 9, 1, 4,
23, 13, 16, 24, 25, 26, 27 | minvecolem4a 29861 |
. . . . 5
β’ (π β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
29 | | eqid 2733 |
. . . . . . 7
β’ (π½ βΎt π) = (π½ βΎt π) |
30 | | nnuz 12811 |
. . . . . . 7
β’ β =
(β€β₯β1) |
31 | 9 | fvexi 6857 |
. . . . . . . 8
β’ π β V |
32 | 31 | a1i 11 |
. . . . . . 7
β’ (π β π β V) |
33 | 16 | mopntop 23809 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β Top) |
34 | 15, 33 | syl 17 |
. . . . . . 7
β’ (π β π½ β Top) |
35 | | xmetres2 23730 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π) β (π· βΎ (π Γ π)) β (βMetβπ)) |
36 | 15, 12, 35 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π· βΎ (π Γ π)) β (βMetβπ)) |
37 | | eqid 2733 |
. . . . . . . . . 10
β’
(MetOpenβ(π·
βΎ (π Γ π))) = (MetOpenβ(π· βΎ (π Γ π))) |
38 | 37 | mopntopon 23808 |
. . . . . . . . 9
β’ ((π· βΎ (π Γ π)) β (βMetβπ) β (MetOpenβ(π· βΎ (π Γ π))) β (TopOnβπ)) |
39 | 36, 38 | syl 17 |
. . . . . . . 8
β’ (π β (MetOpenβ(π· βΎ (π Γ π))) β (TopOnβπ)) |
40 | | lmcl 22664 |
. . . . . . . 8
β’
(((MetOpenβ(π·
βΎ (π Γ π))) β (TopOnβπ) β§ πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) β
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β π) |
41 | 39, 28, 40 | syl2anc 585 |
. . . . . . 7
β’ (π β
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β π) |
42 | | 1zzd 12539 |
. . . . . . 7
β’ (π β 1 β
β€) |
43 | 29, 30, 32, 34, 41, 42, 26 | lmss 22665 |
. . . . . 6
β’ (π β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(π½ βΎt π))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
44 | | eqid 2733 |
. . . . . . . . . 10
β’ (π· βΎ (π Γ π)) = (π· βΎ (π Γ π)) |
45 | 44, 16, 37 | metrest 23896 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
46 | 15, 12, 45 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½ βΎt π) = (MetOpenβ(π· βΎ (π Γ π)))) |
47 | 46 | fveq2d 6847 |
. . . . . . 7
β’ (π β
(βπ‘β(π½ βΎt π)) =
(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))) |
48 | 47 | breqd 5117 |
. . . . . 6
β’ (π β (πΉ(βπ‘β(π½ βΎt π))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
49 | 43, 48 | bitrd 279 |
. . . . 5
β’ (π β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
50 | 28, 49 | mpbird 257 |
. . . 4
β’ (π β πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
51 | | funbrfv 6894 |
. . . 4
β’ (Fun
(βπ‘βπ½) β (πΉ(βπ‘βπ½)((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ) β ((βπ‘βπ½)βπΉ) =
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ))) |
52 | 20, 50, 51 | sylc 65 |
. . 3
β’ (π β
((βπ‘βπ½)βπΉ) =
((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) |
53 | 52, 41 | eqeltrd 2834 |
. 2
β’ (π β
((βπ‘βπ½)βπΉ) β π) |
54 | 12, 53 | sseldd 3946 |
1
β’ (π β
((βπ‘βπ½)βπΉ) β π) |