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 = 𝑠OLD U
lnoval.6 S = 𝑠OLD W
lnoval.7 L = U LnOp W
Assertion lnoval U NrmCVec W NrmCVec L = t Y X | x y X z 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 = 𝑠OLD U
6 lnoval.6 S = 𝑠OLD W
7 lnoval.7 L = U LnOp W
8 fveq2 u = U BaseSet u = BaseSet U
9 8 1 syl6eqr u = U BaseSet u = X
10 9 oveq2d u = U BaseSet w BaseSet u = BaseSet w X
11 fveq2 u = U + v u = + v U
12 11 3 syl6eqr u = U + v u = G
13 fveq2 u = U 𝑠OLD u = 𝑠OLD U
14 13 5 syl6eqr u = U 𝑠OLD u = R
15 14 oveqd u = U x 𝑠OLD u y = x R y
16 eqidd u = U z = z
17 12 15 16 oveq123d u = U x 𝑠OLD u y + v u z = x R y G z
18 17 fveqeq2d u = U t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z t x R y G z = x 𝑠OLD w t y + v w t z
19 9 18 raleqbidv u = U z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z z X t x R y G z = x 𝑠OLD w t y + v w t z
20 9 19 raleqbidv u = U y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z y X z X t x R y G z = x 𝑠OLD w t y + v w t z
21 20 ralbidv u = U x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z x y X z X t x R y G z = x 𝑠OLD w t y + v w t z
22 10 21 rabeqbidv u = U t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z = t BaseSet w X | x y X z X t x R y G z = x 𝑠OLD w t y + v w t z
23 fveq2 w = W BaseSet w = BaseSet W
24 23 2 syl6eqr w = W BaseSet w = Y
25 24 oveq1d w = W BaseSet w X = Y X
26 fveq2 w = W + v w = + v W
27 26 4 syl6eqr w = W + v w = H
28 fveq2 w = W 𝑠OLD w = 𝑠OLD W
29 28 6 syl6eqr w = W 𝑠OLD w = S
30 29 oveqd w = W x 𝑠OLD w t y = x S t y
31 eqidd w = W t z = t z
32 27 30 31 oveq123d w = W x 𝑠OLD 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 𝑠OLD 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 y X z X t x R y G z = x 𝑠OLD w t y + v w t z y X z X t x R y G z = x S t y H t z
35 34 ralbidv w = W x y X z X t x R y G z = x 𝑠OLD w t y + v w t z x y X z X t x R y G z = x S t y H t z
36 25 35 rabeqbidv w = W t BaseSet w X | x y X z X t x R y G z = x 𝑠OLD w t y + v w t z = t Y X | x y X z X t x R y G z = x S t y H t z
37 df-lno LnOp = u NrmCVec , w NrmCVec t BaseSet w BaseSet u | x y BaseSet u z BaseSet u t x 𝑠OLD u y + v u z = x 𝑠OLD w t y + v w t z
38 ovex Y X V
39 38 rabex t Y X | x y X z X t x R y G z = x S t y H t z V
40 22 36 37 39 ovmpo U NrmCVec W NrmCVec U LnOp W = t Y X | x y X z X t x R y G z = x S t y H t z
41 7 40 syl5eq U NrmCVec W NrmCVec L = t Y X | x y X z X t x R y G z = x S t y H t z