Step | Hyp | Ref
| Expression |
1 | | minvec.d |
. . . . . . . 8
β’ π· = ((distβπ) βΎ (π Γ π)) |
2 | 1 | oveqi 7375 |
. . . . . . 7
β’ (π΄π·π₯) = (π΄((distβπ) βΎ (π Γ π))π₯) |
3 | | minvec.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΄ β π) |
5 | | minvec.y |
. . . . . . . . . 10
β’ (π β π β (LSubSpβπ)) |
6 | | minvec.x |
. . . . . . . . . . 11
β’ π = (Baseβπ) |
7 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
8 | 6, 7 | lssss 20413 |
. . . . . . . . . 10
β’ (π β (LSubSpβπ) β π β π) |
9 | 5, 8 | syl 17 |
. . . . . . . . 9
β’ (π β π β π) |
10 | 9 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π₯ β π) |
11 | 4, 10 | ovresd 7526 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π΄((distβπ) βΎ (π Γ π))π₯) = (π΄(distβπ)π₯)) |
12 | 2, 11 | eqtrid 2789 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π΄π·π₯) = (π΄(distβπ)π₯)) |
13 | | minvec.u |
. . . . . . . . 9
β’ (π β π β βPreHil) |
14 | | cphngp 24553 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
NrmGrp) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmGrp) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π β NrmGrp) |
17 | | minvec.n |
. . . . . . . 8
β’ π = (normβπ) |
18 | | minvec.m |
. . . . . . . 8
β’ β =
(-gβπ) |
19 | | eqid 2737 |
. . . . . . . 8
β’
(distβπ) =
(distβπ) |
20 | 17, 6, 18, 19 | ngpds 23976 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π β§ π₯ β π) β (π΄(distβπ)π₯) = (πβ(π΄ β π₯))) |
21 | 16, 4, 10, 20 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π΄(distβπ)π₯) = (πβ(π΄ β π₯))) |
22 | 12, 21 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄π·π₯) = (πβ(π΄ β π₯))) |
23 | 22 | oveq1d 7377 |
. . . 4
β’ ((π β§ π₯ β π) β ((π΄π·π₯)β2) = ((πβ(π΄ β π₯))β2)) |
24 | | minvec.s |
. . . . . . . 8
β’ π = inf(π
, β, < ) |
25 | | minvec.w |
. . . . . . . . . . . 12
β’ (π β (π βΎs π) β CMetSp) |
26 | | minvec.j |
. . . . . . . . . . . 12
β’ π½ = (TopOpenβπ) |
27 | | minvec.r |
. . . . . . . . . . . 12
β’ π
= ran (π¦ β π β¦ (πβ(π΄ β π¦))) |
28 | 6, 18, 17, 13, 5, 25, 3, 26, 27 | minveclem1 24804 |
. . . . . . . . . . 11
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
29 | 28 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
30 | 29 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β β) |
31 | 29 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β β
) |
32 | | 0red 11165 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β 0 β β) |
33 | 29 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β βπ€ β π
0 β€ π€) |
34 | | breq1 5113 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
35 | 34 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
36 | 35 | rspcev 3584 |
. . . . . . . . . 10
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
37 | 32, 33, 36 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
38 | | infrecl 12144 |
. . . . . . . . 9
β’ ((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β inf(π
, β, < ) β
β) |
39 | 30, 31, 37, 38 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β inf(π
, β, < ) β
β) |
40 | 24, 39 | eqeltrid 2842 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π β β) |
41 | 40 | resqcld 14037 |
. . . . . 6
β’ ((π β§ π₯ β π) β (πβ2) β β) |
42 | 41 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β π) β (πβ2) β β) |
43 | 42 | addid1d 11362 |
. . . 4
β’ ((π β§ π₯ β π) β ((πβ2) + 0) = (πβ2)) |
44 | 23, 43 | breq12d 5123 |
. . 3
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β ((πβ(π΄ β π₯))β2) β€ (πβ2))) |
45 | | cphlmod 24554 |
. . . . . . . 8
β’ (π β βPreHil β
π β
LMod) |
46 | 13, 45 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β π β LMod) |
48 | 6, 18 | lmodvsubcl 20383 |
. . . . . 6
β’ ((π β LMod β§ π΄ β π β§ π₯ β π) β (π΄ β π₯) β π) |
49 | 47, 4, 10, 48 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄ β π₯) β π) |
50 | 6, 17 | nmcl 23988 |
. . . . 5
β’ ((π β NrmGrp β§ (π΄ β π₯) β π) β (πβ(π΄ β π₯)) β β) |
51 | 16, 49, 50 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β π) β (πβ(π΄ β π₯)) β β) |
52 | 6, 17 | nmge0 23989 |
. . . . 5
β’ ((π β NrmGrp β§ (π΄ β π₯) β π) β 0 β€ (πβ(π΄ β π₯))) |
53 | 16, 49, 52 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β π) β 0 β€ (πβ(π΄ β π₯))) |
54 | | infregelb 12146 |
. . . . . . 7
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
55 | 30, 31, 37, 32, 54 | syl31anc 1374 |
. . . . . 6
β’ ((π β§ π₯ β π) β (0 β€ inf(π
, β, < ) β βπ€ β π
0 β€ π€)) |
56 | 33, 55 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β π) β 0 β€ inf(π
, β, < )) |
57 | 56, 24 | breqtrrdi 5152 |
. . . 4
β’ ((π β§ π₯ β π) β 0 β€ π) |
58 | 51, 40, 53, 57 | le2sqd 14167 |
. . 3
β’ ((π β§ π₯ β π) β ((πβ(π΄ β π₯)) β€ π β ((πβ(π΄ β π₯))β2) β€ (πβ2))) |
59 | 24 | breq2i 5118 |
. . . 4
β’ ((πβ(π΄ β π₯)) β€ π β (πβ(π΄ β π₯)) β€ inf(π
, β, < )) |
60 | | infregelb 12146 |
. . . . 5
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ (πβ(π΄ β π₯)) β β) β ((πβ(π΄ β π₯)) β€ inf(π
, β, < ) β βπ€ β π
(πβ(π΄ β π₯)) β€ π€)) |
61 | 30, 31, 37, 51, 60 | syl31anc 1374 |
. . . 4
β’ ((π β§ π₯ β π) β ((πβ(π΄ β π₯)) β€ inf(π
, β, < ) β βπ€ β π
(πβ(π΄ β π₯)) β€ π€)) |
62 | 59, 61 | bitrid 283 |
. . 3
β’ ((π β§ π₯ β π) β ((πβ(π΄ β π₯)) β€ π β βπ€ β π
(πβ(π΄ β π₯)) β€ π€)) |
63 | 44, 58, 62 | 3bitr2d 307 |
. 2
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ€ β π
(πβ(π΄ β π₯)) β€ π€)) |
64 | 27 | raleqi 3314 |
. . 3
β’
(βπ€ β
π
(πβ(π΄ β π₯)) β€ π€ β βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))(πβ(π΄ β π₯)) β€ π€) |
65 | | fvex 6860 |
. . . . 5
β’ (πβ(π΄ β π¦)) β V |
66 | 65 | rgenw 3069 |
. . . 4
β’
βπ¦ β
π (πβ(π΄ β π¦)) β V |
67 | | eqid 2737 |
. . . . 5
β’ (π¦ β π β¦ (πβ(π΄ β π¦))) = (π¦ β π β¦ (πβ(π΄ β π¦))) |
68 | | breq2 5114 |
. . . . 5
β’ (π€ = (πβ(π΄ β π¦)) β ((πβ(π΄ β π₯)) β€ π€ β (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) |
69 | 67, 68 | ralrnmptw 7049 |
. . . 4
β’
(βπ¦ β
π (πβ(π΄ β π¦)) β V β (βπ€ β ran (π¦ β π β¦ (πβ(π΄ β π¦)))(πβ(π΄ β π₯)) β€ π€ β βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) |
70 | 66, 69 | ax-mp 5 |
. . 3
β’
(βπ€ β
ran (π¦ β π β¦ (πβ(π΄ β π¦)))(πβ(π΄ β π₯)) β€ π€ β βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
71 | 64, 70 | bitri 275 |
. 2
β’
(βπ€ β
π
(πβ(π΄ β π₯)) β€ π€ β βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦))) |
72 | 63, 71 | bitrdi 287 |
1
β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ¦ β π (πβ(π΄ β π₯)) β€ (πβ(π΄ β π¦)))) |