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 }\leftrightarrow \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	eqtr4di	$$⊢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	eqtr4di	$$⊢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 }\leftrightarrow 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	eqtrid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to B=\left\{t\in L|N\left(t\right)<\mathrm{+\infty }\right\}$$