This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )