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

Metamath Proof Explorer

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 ∈ HrmOp → T : ℋ ⟶ ℋ

Proof

Step Hyp Ref Expression
1 elhmop ⊢ T ∈ HrmOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = T ⁡ x ⋅ ih y
2 1 simplbi ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ