Theorem hmopf

Description: A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopf	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		elhmop	$$⊢T\in \mathrm{HrmOp}\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
2	1	simplbi	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$