# 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}_{\mathrm{OLD}}{W}$
bloval.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
bloval.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion bloval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {B}=\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}$

### Proof

Step Hyp Ref Expression
1 bloval.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
2 bloval.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
3 bloval.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
4 oveq1 ${⊢}{u}={U}\to {u}\mathrm{LnOp}{w}={U}\mathrm{LnOp}{w}$
5 oveq1 ${⊢}{u}={U}\to {u}{normOp}_{\mathrm{OLD}}{w}={U}{normOp}_{\mathrm{OLD}}{w}$
6 5 fveq1d ${⊢}{u}={U}\to \left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)=\left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)$
7 6 breq1d ${⊢}{u}={U}\to \left(\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }↔\left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right)$
8 4 7 rabeqbidv ${⊢}{u}={U}\to \left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}=\left\{{t}\in \left({U}\mathrm{LnOp}{w}\right)|\left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}$
9 oveq2 ${⊢}{w}={W}\to {U}\mathrm{LnOp}{w}={U}\mathrm{LnOp}{W}$
10 9 2 syl6eqr ${⊢}{w}={W}\to {U}\mathrm{LnOp}{w}={L}$
11 oveq2 ${⊢}{w}={W}\to {U}{normOp}_{\mathrm{OLD}}{w}={U}{normOp}_{\mathrm{OLD}}{W}$
12 11 1 syl6eqr ${⊢}{w}={W}\to {U}{normOp}_{\mathrm{OLD}}{w}={N}$
13 12 fveq1d ${⊢}{w}={W}\to \left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)={N}\left({t}\right)$
14 13 breq1d ${⊢}{w}={W}\to \left(\left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }↔{N}\left({t}\right)<\mathrm{+\infty }\right)$
15 10 14 rabeqbidv ${⊢}{w}={W}\to \left\{{t}\in \left({U}\mathrm{LnOp}{w}\right)|\left({U}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}=\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}$
16 df-blo ${⊢}\mathrm{BLnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}\right)$
17 2 ovexi ${⊢}{L}\in \mathrm{V}$
18 17 rabex ${⊢}\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}\in \mathrm{V}$
19 8 15 16 18 ovmpo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}\mathrm{BLnOp}{W}=\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}$
20 3 19 syl5eq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {B}=\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}$