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	$$⊢T\in \mathrm{LinFn}\to T:\mathscr{H}⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ellnfn	$$⊢T\in \mathrm{LinFn}\leftrightarrow \left(T:\mathscr{H}⟶ℂ\wedge \forall x\in ℂ\forall y\in \mathscr{H}\forall z\in \mathscr{H}T\left(\left(x{\cdot }_{ℎ}y\right){+}_{ℎ}z\right)=xT\left(y\right)+T\left(z\right)\right)$$
2	1	simplbi	$$⊢T\in \mathrm{LinFn}\to T:\mathscr{H}⟶ℂ$$