Theorem hhbloi

Description: A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnmo.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhblo.2	$$⊢B=U\mathrm{BLnOp}U$$
Assertion	hhbloi	$$⊢\mathrm{BndLinOp}=B$$

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhblo.2	$$⊢B=U\mathrm{BLnOp}U$$
3		df-bdop	$$⊢\mathrm{BndLinOp}=\left\{x\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(x\right)<\mathrm{+\infty }\right\}$$
4	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
5		eqid	$$⊢U{normOp}_{\mathrm{OLD}}U=U{normOp}_{\mathrm{OLD}}U$$
6	1 5	hhnmoi	$$⊢{norm}_{\mathrm{op}}=U{normOp}_{\mathrm{OLD}}U$$
7		eqid	$$⊢U\mathrm{LnOp}U=U\mathrm{LnOp}U$$
8	1 7	hhlnoi	$$⊢\mathrm{LinOp}=U\mathrm{LnOp}U$$
9	6 8 2	bloval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge U\in \mathrm{NrmCVec}\right)\to B=\left\{x\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(x\right)<\mathrm{+\infty }\right\}$$
10	4 4 9	mp2an	$$⊢B=\left\{x\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(x\right)<\mathrm{+\infty }\right\}$$
11	3 10	eqtr4i	$$⊢\mathrm{BndLinOp}=B$$