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 )