Step | Hyp | Ref
| Expression |
1 | | 0lnfn 30976 |
. . 3
β’ ( β
Γ {0}) β LinFn |
2 | | lnfnf 30875 |
. . 3
β’ ((
β Γ {0}) β LinFn β ( β Γ {0}):
ββΆβ) |
3 | | nmfnval 30867 |
. . 3
β’ ((
β Γ {0}): ββΆβ β (normfnβ(
β Γ {0})) = sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦)))},
β*, < )) |
4 | 1, 2, 3 | mp2b 10 |
. 2
β’
(normfnβ( β Γ {0})) = sup({π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦)))},
β*, < ) |
5 | | c0ex 11157 |
. . . . . . . . . . . 12
β’ 0 β
V |
6 | 5 | fvconst2 7157 |
. . . . . . . . . . 11
β’ (π¦ β β β ((
β Γ {0})βπ¦) = 0) |
7 | 6 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π¦ β β β
(absβ(( β Γ {0})βπ¦)) = (absβ0)) |
8 | | abs0 15179 |
. . . . . . . . . 10
β’
(absβ0) = 0 |
9 | 7, 8 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ β β β
(absβ(( β Γ {0})βπ¦)) = 0) |
10 | 9 | eqeq2d 2744 |
. . . . . . . 8
β’ (π¦ β β β (π₯ = (absβ(( β Γ
{0})βπ¦)) β π₯ = 0)) |
11 | 10 | anbi2d 630 |
. . . . . . 7
β’ (π¦ β β β
(((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦))) β
((normββπ¦) β€ 1 β§ π₯ = 0))) |
12 | 11 | rexbiia 3092 |
. . . . . 6
β’
(βπ¦ β
β ((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦))) β
βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = 0)) |
13 | | ax-hv0cl 29994 |
. . . . . . . 8
β’
0β β β |
14 | | 0le1 11686 |
. . . . . . . 8
β’ 0 β€
1 |
15 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = 0β β
(normββπ¦) =
(normββ0β)) |
16 | | norm0 30119 |
. . . . . . . . . . 11
β’
(normββ0β) =
0 |
17 | 15, 16 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π¦ = 0β β
(normββπ¦) = 0) |
18 | 17 | breq1d 5119 |
. . . . . . . . 9
β’ (π¦ = 0β β
((normββπ¦) β€ 1 β 0 β€ 1)) |
19 | 18 | rspcev 3583 |
. . . . . . . 8
β’
((0β β β β§ 0 β€ 1) β
βπ¦ β β
(normββπ¦) β€ 1) |
20 | 13, 14, 19 | mp2an 691 |
. . . . . . 7
β’
βπ¦ β
β (normββπ¦) β€ 1 |
21 | | r19.41v 3182 |
. . . . . . 7
β’
(βπ¦ β
β ((normββπ¦) β€ 1 β§ π₯ = 0) β (βπ¦ β β
(normββπ¦) β€ 1 β§ π₯ = 0)) |
22 | 20, 21 | mpbiran 708 |
. . . . . 6
β’
(βπ¦ β
β ((normββπ¦) β€ 1 β§ π₯ = 0) β π₯ = 0) |
23 | 12, 22 | bitri 275 |
. . . . 5
β’
(βπ¦ β
β ((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦))) β
π₯ = 0) |
24 | 23 | abbii 2803 |
. . . 4
β’ {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦)))} = {π₯ β£ π₯ = 0} |
25 | | df-sn 4591 |
. . . 4
β’ {0} =
{π₯ β£ π₯ = 0} |
26 | 24, 25 | eqtr4i 2764 |
. . 3
β’ {π₯ β£ βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦)))} =
{0} |
27 | 26 | supeq1i 9391 |
. 2
β’
sup({π₯ β£
βπ¦ β β
((normββπ¦) β€ 1 β§ π₯ = (absβ(( β Γ
{0})βπ¦)))},
β*, < ) = sup({0}, β*, <
) |
28 | | xrltso 13069 |
. . 3
β’ < Or
β* |
29 | | 0xr 11210 |
. . 3
β’ 0 β
β* |
30 | | supsn 9416 |
. . 3
β’ (( <
Or β* β§ 0 β β*) β sup({0},
β*, < ) = 0) |
31 | 28, 29, 30 | mp2an 691 |
. 2
β’ sup({0},
β*, < ) = 0 |
32 | 4, 27, 31 | 3eqtri 2765 |
1
β’
(normfnβ( β Γ {0})) = 0 |