Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nmbdoplb.1 | |
|
Assertion | nmbdoplbi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmbdoplb.1 | |
|
2 | fveq2 | |
|
3 | 2 | fveq2d | |
4 | fveq2 | |
|
5 | 4 | oveq2d | |
6 | 3 5 | breq12d | |
7 | bdopln | |
|
8 | 1 7 | ax-mp | |
9 | 8 | lnopfi | |
10 | 9 | ffvelrni | |
11 | normcl | |
|
12 | 10 11 | syl | |
13 | 12 | adantr | |
14 | 13 | recnd | |
15 | normcl | |
|
16 | 15 | adantr | |
17 | 16 | recnd | |
18 | normne0 | |
|
19 | 18 | biimpar | |
20 | 14 17 19 | divrec2d | |
21 | 16 19 | rereccld | |
22 | 21 | recnd | |
23 | simpl | |
|
24 | 8 | lnopmuli | |
25 | 22 23 24 | syl2anc | |
26 | 25 | fveq2d | |
27 | 10 | adantr | |
28 | norm-iii | |
|
29 | 22 27 28 | syl2anc | |
30 | normgt0 | |
|
31 | 30 | biimpa | |
32 | 16 31 | recgt0d | |
33 | 0re | |
|
34 | ltle | |
|
35 | 33 34 | mpan | |
36 | 21 32 35 | sylc | |
37 | 21 36 | absidd | |
38 | 37 | oveq1d | |
39 | 26 29 38 | 3eqtrrd | |
40 | 20 39 | eqtrd | |
41 | hvmulcl | |
|
42 | 22 23 41 | syl2anc | |
43 | normcl | |
|
44 | 42 43 | syl | |
45 | norm1 | |
|
46 | eqle | |
|
47 | 44 45 46 | syl2anc | |
48 | nmoplb | |
|
49 | 9 48 | mp3an1 | |
50 | 42 47 49 | syl2anc | |
51 | 40 50 | eqbrtrd | |
52 | nmopre | |
|
53 | 1 52 | ax-mp | |
54 | 53 | a1i | |
55 | ledivmul2 | |
|
56 | 13 54 16 31 55 | syl112anc | |
57 | 51 56 | mpbid | |
58 | 0le0 | |
|
59 | 8 | lnop0i | |
60 | 59 | fveq2i | |
61 | norm0 | |
|
62 | 60 61 | eqtri | |
63 | 61 | oveq2i | |
64 | 53 | recni | |
65 | 64 | mul01i | |
66 | 63 65 | eqtri | |
67 | 58 62 66 | 3brtr4i | |
68 | 67 | a1i | |
69 | 6 57 68 | pm2.61ne | |