Metamath Proof Explorer


Theorem bloval

Description: The class of bounded 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 bloval.3 N = U normOp OLD W
bloval.4 L = U LnOp W
bloval.5 B = U BLnOp W
Assertion bloval U NrmCVec W NrmCVec B = t L | N t < +∞

Proof

Step Hyp Ref Expression
1 bloval.3 N = U normOp OLD W
2 bloval.4 L = U LnOp W
3 bloval.5 B = U BLnOp W
4 oveq1 u = U u LnOp w = U LnOp w
5 oveq1 u = U u normOp OLD w = U normOp OLD w
6 5 fveq1d u = U u normOp OLD w t = U normOp OLD w t
7 6 breq1d u = U u normOp OLD w t < +∞ U normOp OLD w t < +∞
8 4 7 rabeqbidv u = U t u LnOp w | u normOp OLD w t < +∞ = t U LnOp w | U normOp OLD w t < +∞
9 oveq2 w = W U LnOp w = U LnOp W
10 9 2 syl6eqr w = W U LnOp w = L
11 oveq2 w = W U normOp OLD w = U normOp OLD W
12 11 1 syl6eqr w = W U normOp OLD w = N
13 12 fveq1d w = W U normOp OLD w t = N t
14 13 breq1d w = W U normOp OLD w t < +∞ N t < +∞
15 10 14 rabeqbidv w = W t U LnOp w | U normOp OLD w t < +∞ = t L | N t < +∞
16 df-blo BLnOp = u NrmCVec , w NrmCVec t u LnOp w | u normOp OLD w t < +∞
17 2 ovexi L V
18 17 rabex t L | N t < +∞ V
19 8 15 16 18 ovmpo U NrmCVec W NrmCVec U BLnOp W = t L | N t < +∞
20 3 19 syl5eq U NrmCVec W NrmCVec B = t L | N t < +∞