# Metamath Proof Explorer

## 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* , < ) )`