Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nmopub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmopval | |
|
2 | 1 | adantr | |
3 | 2 | breq1d | |
4 | nmopsetretALT | |
|
5 | ressxr | |
|
6 | 4 5 | sstrdi | |
7 | supxrleub | |
|
8 | 6 7 | sylan | |
9 | ancom | |
|
10 | eqeq1 | |
|
11 | 10 | anbi1d | |
12 | 9 11 | syl5bb | |
13 | 12 | rexbidv | |
14 | 13 | ralab | |
15 | ralcom4 | |
|
16 | impexp | |
|
17 | 16 | albii | |
18 | fvex | |
|
19 | breq1 | |
|
20 | 19 | imbi2d | |
21 | 18 20 | ceqsalv | |
22 | 17 21 | bitri | |
23 | 22 | ralbii | |
24 | r19.23v | |
|
25 | 24 | albii | |
26 | 15 23 25 | 3bitr3i | |
27 | 14 26 | bitr4i | |
28 | 8 27 | bitrdi | |
29 | 3 28 | bitrd | |