Theorem hhnmoi

Description: The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnmo.1	|- U = <. <. +h , .h >. , normh >.
	hhnmo.2	|- N = ( U normOpOLD U )
Assertion	hhnmoi	|- normop = N

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	|- U = <. <. +h , .h >. , normh >.
2		hhnmo.2	|- N = ( U normOpOLD U )
3		df-nmop	|- normop = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) )
4	1	hhnv	|- U e. NrmCVec
5	1	hhba	|- ~H = ( BaseSet ` U )
6	1	hhnm	|- normh = ( normCV ` U )
7	5 5 6 6 2	nmoofval	|- ( ( U e. NrmCVec /\ U e. NrmCVec ) -> N = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) ) )
8	4 4 7	mp2an	|- N = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) )
9	3 8	eqtr4i	|- normop = N