Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . . . 8
β’ (π β π β
CPreHilOLD) |
2 | | phnv 29798 |
. . . . . . . 8
β’ (π β CPreHilOLD
β π β
NrmCVec) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β π β NrmCVec) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β π β NrmCVec) |
5 | | minveco.a |
. . . . . . 7
β’ (π β π΄ β π) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΄ β π) |
7 | | inss1 4193 |
. . . . . . . . 9
β’
((SubSpβπ)
β© CBan) β (SubSpβπ) |
8 | | minveco.w |
. . . . . . . . 9
β’ (π β π β ((SubSpβπ) β© CBan)) |
9 | 7, 8 | sselid 3947 |
. . . . . . . 8
β’ (π β π β (SubSpβπ)) |
10 | | minveco.x |
. . . . . . . . 9
β’ π = (BaseSetβπ) |
11 | | minveco.y |
. . . . . . . . 9
β’ π = (BaseSetβπ) |
12 | | eqid 2737 |
. . . . . . . . 9
β’
(SubSpβπ) =
(SubSpβπ) |
13 | 10, 11, 12 | sspba 29711 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
14 | 3, 9, 13 | syl2anc 585 |
. . . . . . 7
β’ (π β π β π) |
15 | 14 | sselda 3949 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β π) |
16 | | minveco.m |
. . . . . . 7
β’ π = ( βπ£
βπ) |
17 | | minveco.n |
. . . . . . 7
β’ π =
(normCVβπ) |
18 | | minveco.d |
. . . . . . 7
β’ π· = (IndMetβπ) |
19 | 10, 16, 17, 18 | imsdval 29670 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π₯ β π) β (π΄π·π₯) = (πβ(π΄ππ₯))) |
20 | 4, 6, 15, 19 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄π·π₯) = (πβ(π΄ππ₯))) |
21 | 20 | oveq1d 7377 |
. . . 4
β’ ((π β§ π₯ β π) β ((π΄π·π₯)β2) = ((πβ(π΄ππ₯))β2)) |
22 | | minveco.s |
. . . . . . . 8
β’ π = inf(π
, β, < ) |
23 | | minveco.j |
. . . . . . . . . . . 12
β’ π½ = (MetOpenβπ·) |
24 | | minveco.r |
. . . . . . . . . . . 12
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
25 | 10, 16, 17, 11, 1, 8, 5, 18, 23, 24 | minvecolem1 29858 |
. . . . . . . . . . 11
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
27 | 26 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β β) |
28 | 26 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β β
) |
29 | | 0red 11165 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β 0 β β) |
30 | 26 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β βπ€ β π
0 β€ π€) |
31 | | breq1 5113 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
32 | 31 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
33 | 32 | rspcev 3584 |
. . . . . . . . . 10
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
34 | 29, 30, 33 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
35 | | infrecl 12144 |
. . . . . . . . 9
β’ ((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β inf(π
, β, < ) β
β) |
36 | 27, 28, 34, 35 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β inf(π
, β, < ) β
β) |
37 | 22, 36 | eqeltrid 2842 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π β β) |
38 | 37 | resqcld 14037 |
. . . . . 6
β’ ((π β§ π₯ β π) β (πβ2) β β) |
39 | 38 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β π) β (πβ2) β β) |
40 | 39 | addid1d 11362 |
. . . 4
β’ ((π β§ π₯ β π) β ((πβ2) + 0) = (πβ2)) |
41 | 21, 40 | breq12d 5123 |
. . 3
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β ((πβ(π΄ππ₯))β2) β€ (πβ2))) |
42 | 10, 16 | nvmcl 29630 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π₯ β π) β (π΄ππ₯) β π) |
43 | 4, 6, 15, 42 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄ππ₯) β π) |
44 | 10, 17 | nvcl 29645 |
. . . . 5
β’ ((π β NrmCVec β§ (π΄ππ₯) β π) β (πβ(π΄ππ₯)) β β) |
45 | 4, 43, 44 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β π) β (πβ(π΄ππ₯)) β β) |
46 | 10, 17 | nvge0 29657 |
. . . . 5
β’ ((π β NrmCVec β§ (π΄ππ₯) β π) β 0 β€ (πβ(π΄ππ₯))) |
47 | 4, 43, 46 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β π) β 0 β€ (πβ(π΄ππ₯))) |
48 | | infregelb 12146 |
. . . . . . 7
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
49 | 27, 28, 34, 29, 48 | syl31anc 1374 |
. . . . . 6
β’ ((π β§ π₯ β π) β (0 β€ inf(π
, β, < ) β βπ€ β π
0 β€ π€)) |
50 | 30, 49 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β π) β 0 β€ inf(π
, β, < )) |
51 | 50, 22 | breqtrrdi 5152 |
. . . 4
β’ ((π β§ π₯ β π) β 0 β€ π) |
52 | 45, 37, 47, 51 | le2sqd 14167 |
. . 3
β’ ((π β§ π₯ β π) β ((πβ(π΄ππ₯)) β€ π β ((πβ(π΄ππ₯))β2) β€ (πβ2))) |
53 | 22 | breq2i 5118 |
. . . 4
β’ ((πβ(π΄ππ₯)) β€ π β (πβ(π΄ππ₯)) β€ inf(π
, β, < )) |
54 | | infregelb 12146 |
. . . . 5
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ (πβ(π΄ππ₯)) β β) β ((πβ(π΄ππ₯)) β€ inf(π
, β, < ) β βπ€ β π
(πβ(π΄ππ₯)) β€ π€)) |
55 | 27, 28, 34, 45, 54 | syl31anc 1374 |
. . . 4
β’ ((π β§ π₯ β π) β ((πβ(π΄ππ₯)) β€ inf(π
, β, < ) β βπ€ β π
(πβ(π΄ππ₯)) β€ π€)) |
56 | 53, 55 | bitrid 283 |
. . 3
β’ ((π β§ π₯ β π) β ((πβ(π΄ππ₯)) β€ π β βπ€ β π
(πβ(π΄ππ₯)) β€ π€)) |
57 | 41, 52, 56 | 3bitr2d 307 |
. 2
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ€ β π
(πβ(π΄ππ₯)) β€ π€)) |
58 | 24 | raleqi 3314 |
. . 3
β’
(βπ€ β
π
(πβ(π΄ππ₯)) β€ π€ β βπ€ β ran (π¦ β π β¦ (πβ(π΄ππ¦)))(πβ(π΄ππ₯)) β€ π€) |
59 | | fvex 6860 |
. . . . 5
β’ (πβ(π΄ππ¦)) β V |
60 | 59 | rgenw 3069 |
. . . 4
β’
βπ¦ β
π (πβ(π΄ππ¦)) β V |
61 | | eqid 2737 |
. . . . 5
β’ (π¦ β π β¦ (πβ(π΄ππ¦))) = (π¦ β π β¦ (πβ(π΄ππ¦))) |
62 | | breq2 5114 |
. . . . 5
β’ (π€ = (πβ(π΄ππ¦)) β ((πβ(π΄ππ₯)) β€ π€ β (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) |
63 | 61, 62 | ralrnmptw 7049 |
. . . 4
β’
(βπ¦ β
π (πβ(π΄ππ¦)) β V β (βπ€ β ran (π¦ β π β¦ (πβ(π΄ππ¦)))(πβ(π΄ππ₯)) β€ π€ β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) |
64 | 60, 63 | ax-mp 5 |
. . 3
β’
(βπ€ β
ran (π¦ β π β¦ (πβ(π΄ππ¦)))(πβ(π΄ππ₯)) β€ π€ β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |
65 | 58, 64 | bitri 275 |
. 2
β’
(βπ€ β
π
(πβ(π΄ππ₯)) β€ π€ β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |
66 | 57, 65 | bitrdi 287 |
1
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) |