Description: A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nmcfnlb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | fveq1 | |
|
3 | 2 | fveq2d | |
4 | fveq2 | |
|
5 | 4 | oveq1d | |
6 | 3 5 | breq12d | |
7 | 6 | imbi2d | |
8 | 0lnfn | |
|
9 | 0cnfn | |
|
10 | elin | |
|
11 | 8 9 10 | mpbir2an | |
12 | 11 | elimel | |
13 | elin | |
|
14 | 12 13 | mpbi | |
15 | 14 | simpli | |
16 | 14 | simpri | |
17 | 15 16 | nmcfnlbi | |
18 | 7 17 | dedth | |
19 | 18 | imp | |
20 | 1 19 | sylanbr | |
21 | 20 | 3impa | |