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