Metamath Proof Explorer


Theorem nmopge0

Description: The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopge0 T:0normopT

Proof

Step Hyp Ref Expression
1 ax-hv0cl 0
2 ffvelrn T:0T0
3 1 2 mpan2 T:T0
4 normge0 T00normT0
5 3 4 syl T:0normT0
6 norm0 norm0=0
7 0le1 01
8 6 7 eqbrtri norm01
9 nmoplb T:0norm01normT0normopT
10 1 8 9 mp3an23 T:normT0normopT
11 normcl T0normT0
12 3 11 syl T:normT0
13 12 rexrd T:normT0*
14 nmopxr T:normopT*
15 0xr 0*
16 xrletr 0*normT0*normopT*0normT0normT0normopT0normopT
17 15 16 mp3an1 normT0*normopT*0normT0normT0normopT0normopT
18 13 14 17 syl2anc T:0normT0normT0normopT0normopT
19 5 10 18 mp2and T:0normopT