This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmfnval

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

Ref Expression
Assertion nmfnval 
|- ( T : ~H --> CC -> ( normfn ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( 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 = ( abs ` ( T ` y ) ) ) } , RR* , < ) e. _V
3 ax-hilex 
 |-  ~H e. _V
4 cnex 
 |-  CC e. _V
5 fveq1 
 |-  ( t = T -> ( t ` y ) = ( T ` y ) )
6 5 fveq2d 
 |-  ( t = T -> ( abs ` ( t ` y ) ) = ( abs ` ( T ` y ) ) )
7 6 eqeq2d 
 |-  ( t = T -> ( x = ( abs ` ( t ` y ) ) <-> x = ( abs ` ( T ` y ) ) ) )
8 7 anbi2d 
 |-  ( t = T -> ( ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( t ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) ) )
9 8 rexbidv 
 |-  ( t = T -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( t ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) ) )
10 9 abbidv 
 |-  ( t = T -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( t ` y ) ) ) } = { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } )
11 10 supeq1d 
 |-  ( t = T -> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( t ` y ) ) ) } , RR* , < ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) )
12 df-nmfn 
 |-  normfn = ( t e. ( CC ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( t ` y ) ) ) } , RR* , < ) )
13 2 3 4 11 12 fvmptmap 
 |-  ( T : ~H --> CC -> ( normfn ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) )