Theorem nmopval

Description: Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopval	|- ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		xrltso	|- < Or RR*
2	1	supex	|- sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) e. _V
3		ax-hilex	|- ~H e. _V
4		fveq1	|- ( t = T -> ( t ` y ) = ( T ` y ) )
5	4	fveq2d	|- ( t = T -> ( normh ` ( t ` y ) ) = ( normh ` ( T ` y ) ) )
6	5	eqeq2d	|- ( t = T -> ( x = ( normh ` ( t ` y ) ) <-> x = ( normh ` ( T ` y ) ) ) )
7	6	anbi2d	|- ( t = T -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) ) )
8	7	rexbidv	|- ( t = T -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) ) )
9	8	abbidv	|- ( t = T -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } = { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } )
10	9	supeq1d	|- ( t = T -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
11		df-nmop	|- normop = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) )
12	2 3 3 10 11	fvmptmap	|- ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )