Metamath Proof Explorer

Theorem nmoofval

Description: The operator norm function. (Contributed by NM, 6-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 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* , < ) ) )

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 fveq2 
 |-  ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
7 6 1 eqtr4di 
 |-  ( u = U -> ( BaseSet ` u ) = X )
8 7 oveq2d 
 |-  ( u = U -> ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) = ( ( BaseSet ` w ) ^m X ) )
9 fveq2 
 |-  ( u = U -> ( normCV ` u ) = ( normCV ` U ) )
10 9 3 eqtr4di 
 |-  ( u = U -> ( normCV ` u ) = L )
11 10 fveq1d 
 |-  ( u = U -> ( ( normCV ` u ) ` z ) = ( L ` z ) )
12 11 breq1d 
 |-  ( u = U -> ( ( ( normCV ` u ) ` z ) <_ 1 <-> ( L ` z ) <_ 1 ) )
13 12 anbi1d 
 |-  ( u = U -> ( ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) <-> ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) ) )
14 7 13 rexeqbidv 
 |-  ( u = U -> ( E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) <-> E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) ) )
15 14 abbidv 
 |-  ( u = U -> { x | E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } = { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } )
16 15 supeq1d 
 |-  ( u = U -> sup ( { x | E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) )
17 8 16 mpteq12dv 
 |-  ( u = U -> ( t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) |-> sup ( { x | E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) ) = ( t e. ( ( BaseSet ` w ) ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) ) )
18 fveq2 
 |-  ( w = W -> ( BaseSet ` w ) = ( BaseSet ` W ) )
19 18 2 eqtr4di 
 |-  ( w = W -> ( BaseSet ` w ) = Y )
20 19 oveq1d 
 |-  ( w = W -> ( ( BaseSet ` w ) ^m X ) = ( Y ^m X ) )
21 fveq2 
 |-  ( w = W -> ( normCV ` w ) = ( normCV ` W ) )
22 21 4 eqtr4di 
 |-  ( w = W -> ( normCV ` w ) = M )
23 22 fveq1d 
 |-  ( w = W -> ( ( normCV ` w ) ` ( t ` z ) ) = ( M ` ( t ` z ) ) )
24 23 eqeq2d 
 |-  ( w = W -> ( x = ( ( normCV ` w ) ` ( t ` z ) ) <-> x = ( M ` ( t ` z ) ) ) )
25 24 anbi2d 
 |-  ( w = W -> ( ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) <-> ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) ) )
26 25 rexbidv 
 |-  ( w = W -> ( E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) <-> E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) ) )
27 26 abbidv 
 |-  ( w = W -> { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } = { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } )
28 27 supeq1d 
 |-  ( w = W -> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) = sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) )
29 20 28 mpteq12dv 
 |-  ( w = W -> ( t e. ( ( BaseSet ` w ) ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) ) = ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) )
30 df-nmoo 
 |-  normOpOLD = ( u e. NrmCVec , w e. NrmCVec |-> ( t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) |-> sup ( { x | E. z e. ( BaseSet ` u ) ( ( ( normCV ` u ) ` z ) <_ 1 /\ x = ( ( normCV ` w ) ` ( t ` z ) ) ) } , RR* , < ) ) )
31 ovex 
 |-  ( Y ^m X ) e. _V
32 31 mptex 
 |-  ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) e. _V
33 17 29 30 32 ovmpo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U normOpOLD W ) = ( t e. ( Y ^m X ) |-> sup ( { x | E. z e. X ( ( L ` z ) <_ 1 /\ x = ( M ` ( t ` z ) ) ) } , RR* , < ) ) )
34 5 33 syl5eq 
 |-  ( ( 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* , < ) ) )