Metamath Proof Explorer

Theorem lnoval

Description: The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnoval.1 
|- X = ( BaseSet ` U )
lnoval.2 
|- Y = ( BaseSet ` W )
lnoval.3 
|- G = ( +v ` U )
lnoval.4 
|- H = ( +v ` W )
lnoval.5 
|- R = ( .sOLD ` U )
lnoval.6 
|- S = ( .sOLD ` W )
lnoval.7 
|- L = ( U LnOp W )
Assertion lnoval 
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> L = { t e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) } )

Proof

Step Hyp Ref Expression
1 lnoval.1 
 |-  X = ( BaseSet ` U )
2 lnoval.2 
 |-  Y = ( BaseSet ` W )
3 lnoval.3 
 |-  G = ( +v ` U )
4 lnoval.4 
 |-  H = ( +v ` W )
5 lnoval.5 
 |-  R = ( .sOLD ` U )
6 lnoval.6 
 |-  S = ( .sOLD ` W )
7 lnoval.7 
 |-  L = ( U LnOp W )
8 fveq2 
 |-  ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
9 8 1 eqtr4di 
 |-  ( u = U -> ( BaseSet ` u ) = X )
10 9 oveq2d 
 |-  ( u = U -> ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) = ( ( BaseSet ` w ) ^m X ) )
11 fveq2 
 |-  ( u = U -> ( +v ` u ) = ( +v ` U ) )
12 11 3 eqtr4di 
 |-  ( u = U -> ( +v ` u ) = G )
13 fveq2 
 |-  ( u = U -> ( .sOLD ` u ) = ( .sOLD ` U ) )
14 13 5 eqtr4di 
 |-  ( u = U -> ( .sOLD ` u ) = R )
15 14 oveqd 
 |-  ( u = U -> ( x ( .sOLD ` u ) y ) = ( x R y ) )
16 eqidd 
 |-  ( u = U -> z = z )
17 12 15 16 oveq123d 
 |-  ( u = U -> ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) = ( ( x R y ) G z ) )
18 17 fveqeq2d 
 |-  ( u = U -> ( ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) ) )
19 9 18 raleqbidv 
 |-  ( u = U -> ( A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) ) )
20 9 19 raleqbidv 
 |-  ( u = U -> ( A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) ) )
21 20 ralbidv 
 |-  ( u = U -> ( A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) ) )
22 10 21 rabeqbidv 
 |-  ( u = U -> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } = { t e. ( ( BaseSet ` w ) ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )
23 fveq2 
 |-  ( w = W -> ( BaseSet ` w ) = ( BaseSet ` W ) )
24 23 2 eqtr4di 
 |-  ( w = W -> ( BaseSet ` w ) = Y )
25 24 oveq1d 
 |-  ( w = W -> ( ( BaseSet ` w ) ^m X ) = ( Y ^m X ) )
26 fveq2 
 |-  ( w = W -> ( +v ` w ) = ( +v ` W ) )
27 26 4 eqtr4di 
 |-  ( w = W -> ( +v ` w ) = H )
28 fveq2 
 |-  ( w = W -> ( .sOLD ` w ) = ( .sOLD ` W ) )
29 28 6 eqtr4di 
 |-  ( w = W -> ( .sOLD ` w ) = S )
30 29 oveqd 
 |-  ( w = W -> ( x ( .sOLD ` w ) ( t ` y ) ) = ( x S ( t ` y ) ) )
31 eqidd 
 |-  ( w = W -> ( t ` z ) = ( t ` z ) )
32 27 30 31 oveq123d 
 |-  ( w = W -> ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) )
33 32 eqeq2d 
 |-  ( w = W -> ( ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) ) )
34 33 2ralbidv 
 |-  ( w = W -> ( A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) ) )
35 34 ralbidv 
 |-  ( w = W -> ( A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) <-> A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) ) )
36 25 35 rabeqbidv 
 |-  ( w = W -> { t e. ( ( BaseSet ` w ) ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } = { t e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) } )
37 df-lno 
 |-  LnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( ( BaseSet ` w ) ^m ( BaseSet ` u ) ) | A. x e. CC A. y e. ( BaseSet ` u ) A. z e. ( BaseSet ` u ) ( t ` ( ( x ( .sOLD ` u ) y ) ( +v ` u ) z ) ) = ( ( x ( .sOLD ` w ) ( t ` y ) ) ( +v ` w ) ( t ` z ) ) } )
38 ovex 
 |-  ( Y ^m X ) e. _V
39 38 rabex 
 |-  { t e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) } e. _V
40 22 36 37 39 ovmpo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U LnOp W ) = { t e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) } )
41 7 40 syl5eq 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> L = { t e. ( Y ^m X ) | A. x e. CC A. y e. X A. z e. X ( t ` ( ( x R y ) G z ) ) = ( ( x S ( t ` y ) ) H ( t ` z ) ) } )