Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | lnopf | ⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ellnop | ⊢ ( 𝑇 ∈ LinOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·_{ℎ} 𝑦 ) +_{ℎ} 𝑧 ) ) = ( ( 𝑥 ·_{ℎ} ( 𝑇 ‘ 𝑦 ) ) +_{ℎ} ( 𝑇 ‘ 𝑧 ) ) ) ) | |
2 | 1 | simplbi | ⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ ) |