Description: The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nmopge0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hv0cl | |
|
2 | ffvelrn | |
|
3 | 1 2 | mpan2 | |
4 | normge0 | |
|
5 | 3 4 | syl | |
6 | norm0 | |
|
7 | 0le1 | |
|
8 | 6 7 | eqbrtri | |
9 | nmoplb | |
|
10 | 1 8 9 | mp3an23 | |
11 | normcl | |
|
12 | 3 11 | syl | |
13 | 12 | rexrd | |
14 | nmopxr | |
|
15 | 0xr | |
|
16 | xrletr | |
|
17 | 15 16 | mp3an1 | |
18 | 13 14 17 | syl2anc | |
19 | 5 10 18 | mp2and | |