This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∣ ( norm_op ‘ 𝑥 ) < +∞ }
4	1	hhnv	⊢ 𝑈 ∈ NrmCVec
5		eqid	⊢ ( 𝑈 normOp_OLD 𝑈 ) = ( 𝑈 normOp_OLD 𝑈 )
6	1 5	hhnmoi	⊢ norm_op = ( 𝑈 normOp_OLD 𝑈 )
7		eqid	⊢ ( 𝑈 LnOp 𝑈 ) = ( 𝑈 LnOp 𝑈 )
8	1 7	hhlnoi	⊢ LinOp = ( 𝑈 LnOp 𝑈 )
9	6 8 2	bloval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝐵 = { 𝑥 ∈ LinOp ∣ ( norm_op ‘ 𝑥 ) < +∞ } )
10	4 4 9	mp2an	⊢ 𝐵 = { 𝑥 ∈ LinOp ∣ ( norm_op ‘ 𝑥 ) < +∞ }
11	3 10	eqtr4i	⊢ BndLinOp = 𝐵