Description: Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nmofval.1 | |
|
nmofval.2 | |
||
nmofval.3 | |
||
nmofval.4 | |
||
nmolb2d.z | |
||
nmolb2d.1 | |
||
nmolb2d.2 | |
||
nmolb2d.3 | |
||
nmolb2d.4 | |
||
nmolb2d.5 | |
||
nmolb2d.6 | |
||
Assertion | nmolb2d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmofval.1 | |
|
2 | nmofval.2 | |
|
3 | nmofval.3 | |
|
4 | nmofval.4 | |
|
5 | nmolb2d.z | |
|
6 | nmolb2d.1 | |
|
7 | nmolb2d.2 | |
|
8 | nmolb2d.3 | |
|
9 | nmolb2d.4 | |
|
10 | nmolb2d.5 | |
|
11 | nmolb2d.6 | |
|
12 | 2fveq3 | |
|
13 | fveq2 | |
|
14 | 13 | oveq2d | |
15 | 12 14 | breq12d | |
16 | 11 | anassrs | |
17 | 0le0 | |
|
18 | 9 | recnd | |
19 | 18 | mul01d | |
20 | 17 19 | breqtrrid | |
21 | eqid | |
|
22 | 5 21 | ghmid | |
23 | 8 22 | syl | |
24 | 23 | fveq2d | |
25 | 4 21 | nm0 | |
26 | 7 25 | syl | |
27 | 24 26 | eqtrd | |
28 | 3 5 | nm0 | |
29 | 6 28 | syl | |
30 | 29 | oveq2d | |
31 | 20 27 30 | 3brtr4d | |
32 | 31 | adantr | |
33 | 15 16 32 | pm2.61ne | |
34 | 33 | ralrimiva | |
35 | 1 2 3 4 | nmolb | |
36 | 6 7 8 9 10 35 | syl311anc | |
37 | 34 36 | mpd | |