# 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 ) ) } )`