Theorem lnfnf

Description: A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnfnf	⊢ ( 𝑇 ∈ LinFn → 𝑇 : ℋ ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ellnfn	⊢ ( 𝑇 ∈ LinFn ↔ ( 𝑇 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝑇 ‘ 𝑦 ) ) + ( 𝑇 ‘ 𝑧 ) ) ) )
2	1	simplbi	⊢ ( 𝑇 ∈ LinFn → 𝑇 : ℋ ⟶ ℂ )