Description: A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nmcopex.1 | |
|
nmcopex.2 | |
||
Assertion | nmcoplbi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmcopex.1 | |
|
2 | nmcopex.2 | |
|
3 | 0le0 | |
|
4 | 3 | a1i | |
5 | fveq2 | |
|
6 | 1 | lnop0i | |
7 | 5 6 | eqtrdi | |
8 | 7 | fveq2d | |
9 | norm0 | |
|
10 | 8 9 | eqtrdi | |
11 | fveq2 | |
|
12 | 11 9 | eqtrdi | |
13 | 12 | oveq2d | |
14 | 1 2 | nmcopexi | |
15 | 14 | recni | |
16 | 15 | mul01i | |
17 | 13 16 | eqtrdi | |
18 | 4 10 17 | 3brtr4d | |
19 | 18 | adantl | |
20 | normcl | |
|
21 | 20 | adantr | |
22 | normne0 | |
|
23 | 22 | biimpar | |
24 | 21 23 | rereccld | |
25 | normgt0 | |
|
26 | 25 | biimpa | |
27 | 21 26 | recgt0d | |
28 | 0re | |
|
29 | ltle | |
|
30 | 28 29 | mpan | |
31 | 24 27 30 | sylc | |
32 | 24 31 | absidd | |
33 | 32 | oveq1d | |
34 | 24 | recnd | |
35 | simpl | |
|
36 | 1 | lnopmuli | |
37 | 34 35 36 | syl2anc | |
38 | 37 | fveq2d | |
39 | 1 | lnopfi | |
40 | 39 | ffvelrni | |
41 | 40 | adantr | |
42 | norm-iii | |
|
43 | 34 41 42 | syl2anc | |
44 | 38 43 | eqtrd | |
45 | normcl | |
|
46 | 40 45 | syl | |
47 | 46 | adantr | |
48 | 47 | recnd | |
49 | 21 | recnd | |
50 | 48 49 23 | divrec2d | |
51 | 33 44 50 | 3eqtr4rd | |
52 | hvmulcl | |
|
53 | 34 35 52 | syl2anc | |
54 | normcl | |
|
55 | 53 54 | syl | |
56 | norm1 | |
|
57 | eqle | |
|
58 | 55 56 57 | syl2anc | |
59 | nmoplb | |
|
60 | 39 59 | mp3an1 | |
61 | 53 58 60 | syl2anc | |
62 | 51 61 | eqbrtrd | |
63 | 14 | a1i | |
64 | ledivmul2 | |
|
65 | 47 63 21 26 64 | syl112anc | |
66 | 62 65 | mpbid | |
67 | 19 66 | pm2.61dane | |