Metamath Proof Explorer


Theorem nmop0h

Description: The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ~H =/= 0H in nmopun .) (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmop0h = 0 T : norm op T = 0

Proof

Step Hyp Ref Expression
1 df-ch0 0 = 0
2 1 eqeq2i = 0 = 0
3 feq3 = 0 T : T : 0
4 2 3 sylbi = 0 T : T : 0
5 ax-hv0cl 0
6 5 elexi 0 V
7 6 fconst2 T : 0 T = × 0
8 df0op2 0 hop = × 0
9 1 xpeq2i × 0 = × 0
10 8 9 eqtri 0 hop = × 0
11 10 eqeq2i T = 0 hop T = × 0
12 7 11 bitr4i T : 0 T = 0 hop
13 4 12 bitrdi = 0 T : T = 0 hop
14 13 biimpa = 0 T : T = 0 hop
15 14 fveq2d = 0 T : norm op T = norm op 0 hop
16 nmop0 norm op 0 hop = 0
17 15 16 eqtrdi = 0 T : norm op T = 0