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
|- ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = 0 )

Proof

Step Hyp Ref Expression
1 df-ch0
 |-  0H = { 0h }
2 1 eqeq2i
 |-  ( ~H = 0H <-> ~H = { 0h } )
3 feq3
 |-  ( ~H = { 0h } -> ( T : ~H --> ~H <-> T : ~H --> { 0h } ) )
4 2 3 sylbi
 |-  ( ~H = 0H -> ( T : ~H --> ~H <-> T : ~H --> { 0h } ) )
5 ax-hv0cl
 |-  0h e. ~H
6 5 elexi
 |-  0h e. _V
7 6 fconst2
 |-  ( T : ~H --> { 0h } <-> T = ( ~H X. { 0h } ) )
8 df0op2
 |-  0hop = ( ~H X. 0H )
9 1 xpeq2i
 |-  ( ~H X. 0H ) = ( ~H X. { 0h } )
10 8 9 eqtri
 |-  0hop = ( ~H X. { 0h } )
11 10 eqeq2i
 |-  ( T = 0hop <-> T = ( ~H X. { 0h } ) )
12 7 11 bitr4i
 |-  ( T : ~H --> { 0h } <-> T = 0hop )
13 4 12 bitrdi
 |-  ( ~H = 0H -> ( T : ~H --> ~H <-> T = 0hop ) )
14 13 biimpa
 |-  ( ( ~H = 0H /\ T : ~H --> ~H ) -> T = 0hop )
15 14 fveq2d
 |-  ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = ( normop ` 0hop ) )
16 nmop0
 |-  ( normop ` 0hop ) = 0
17 15 16 eqtrdi
 |-  ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = 0 )