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	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
		hhblo.2	$⊢ B = U BLnOp U$
	Assertion	hhbloi	$⊢ BndLinOp = B$

Proof

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