Metamath Proof Explorer

Theorem nmooval

Description: The operator norm function. (Contributed by NM, 27-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoofval.1 
|- X = ( BaseSet ` U )
nmoofval.2 
|- Y = ( BaseSet ` W )
nmoofval.3 
|- L = ( normCV ` U )
nmoofval.4 
|- M = ( normCV ` W )
nmoofval.6 
|- N = ( U normOpOLD W )
Assertion nmooval 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )

Proof

Step Hyp Ref Expression
1 nmoofval.1 
 |-  X = ( BaseSet ` U )
2 nmoofval.2 
 |-  Y = ( BaseSet ` W )
3 nmoofval.3 
 |-  L = ( normCV ` U )
4 nmoofval.4 
 |-  M = ( normCV ` W )
5 nmoofval.6 
 |-  N = ( U normOpOLD W )
6 2 fvexi 
 |-  Y e. _V
7 1 fvexi 
 |-  X e. _V
8 6 7 elmap 
 |-  ( T e. ( Y ^m X ) <-> T : X --> Y )
9 1 2 3 4 5 nmoofval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> N = ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) )
10 9 fveq1d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( N ` T ) = ( ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) ` T ) )
11 fveq1 
 |-  ( t = T -> ( t ` z ) = ( T ` z ) )
12 11 fveq2d 
 |-  ( t = T -> ( M ` ( t ` z ) ) = ( M ` ( T ` z ) ) )
13 12 eqeq2d 
 |-  ( t = T -> ( x = ( M ` ( t ` z ) ) <-> x = ( M ` ( T ` z ) ) ) )
14 13 anbi2d 
 |-  ( t = T -> ( ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) <-> ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) ) )
15 14 rexbidv 
 |-  ( t = T -> ( E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) <-> E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) ) )
16 15 abbidv 
 |-  ( t = T -> { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } = { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } )
17 16 supeq1d 
 |-  ( t = T -> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )
18 eqid 
 |-  ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) = ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) )
19 xrltso 
 |-  < Or RR*
20 19 supex 
 |-  sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) e. _V
21 17 18 20 fvmpt 
 |-  ( T e. ( Y ^m X ) -> ( ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) ` T ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )
22 10 21 sylan9eq 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ T e. ( Y ^m X ) ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )
23 8 22 sylan2br 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )
24 23 3impa 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( T ` z ) ) ) } , RR* , < ) )