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	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhblo.2	⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
Assertion	hhbloi	⊢ BndLinOp = 𝐵

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhblo.2	⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
3		df-bdop	⊢ BndLinOp = { 𝑥 ∈ LinOp ∣ ( normop ‘ 𝑥 ) < +∞ }
4	1	hhnv	⊢ 𝑈 ∈ NrmCVec
5		eqid	⊢ ( 𝑈 normOpOLD 𝑈 ) = ( 𝑈 normOpOLD 𝑈 )
6	1 5	hhnmoi	⊢ normop = ( 𝑈 normOpOLD 𝑈 )
7		eqid	⊢ ( 𝑈 LnOp 𝑈 ) = ( 𝑈 LnOp 𝑈 )
8	1 7	hhlnoi	⊢ LinOp = ( 𝑈 LnOp 𝑈 )
9	6 8 2	bloval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝐵 = { 𝑥 ∈ LinOp ∣ ( normop ‘ 𝑥 ) < +∞ } )
10	4 4 9	mp2an	⊢ 𝐵 = { 𝑥 ∈ LinOp ∣ ( normop ‘ 𝑥 ) < +∞ }
11	3 10	eqtr4i	⊢ BndLinOp = 𝐵