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

Metamath Proof Explorer

Definition df-nmfn

Description: Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion df-nmfn 
|- normfn = ( t e. ( CC ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) } , RR* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmf 
 |-  normfn
1 vt 
 |-  t
2 cc 
 |-  CC
3 cmap 
 |-  ^m
4 chba 
 |-  ~H
5 2 4 3 co 
 |-  ( CC ^m ~H )
6 vx 
 |-  x
7 vz 
 |-  z
8 cno 
 |-  normh
9 7 cv 
 |-  z
10 9 8 cfv 
 |-  ( normh ` z )
11 cle 
 |-  <_
12 c1 
 |-  1
13 10 12 11 wbr 
 |-  ( normh ` z ) <_ 1
14 6 cv 
 |-  x
15 cabs 
 |-  abs
16 1 cv 
 |-  t
17 9 16 cfv 
 |-  ( t ` z )
18 17 15 cfv 
 |-  ( abs ` ( t ` z ) )
19 14 18 wceq 
 |-  x = ( abs ` ( t ` z ) )
20 13 19 wa 
 |-  ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) )
21 20 7 4 wrex 
 |-  E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) )
22 21 6 cab 
 |-  { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) }
23 cxr 
 |-  RR*
24 clt 
 |-  <
25 22 23 24 csup 
 |-  sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) } , RR* , < )
26 1 5 25 cmpt 
 |-  ( t e. ( CC ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) } , RR* , < ) )
27 0 26 wceq 
 |-  normfn = ( t e. ( CC ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( abs ` ( t ` z ) ) ) } , RR* , < ) )