Metamath Proof Explorer

Definition df-nmop

Description: Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

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

Detailed syntax breakdown

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