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 eqtr4di ⊢ w = W → U LnOp w = L
11 oveq2 ⊢ w = W → U normOp OLD w = U normOp OLD W
12 11 1 eqtr4di ⊢ 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 < +∞