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	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )

Proof

Step	Hyp	Ref	Expression
1		elhmop	⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
2	1	simplbi	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )