Theorem lnop0i

Description: The value of a linear Hilbert space operator at zero is zero. Remark in Beran p. 99. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopl.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnop0i	$$⊢T\left(0_{ℎ}\right)=0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	$$⊢T\in \mathrm{LinOp}$$
2		lnop0	$$⊢T\in \mathrm{LinOp}\to T\left(0_{ℎ}\right)=0_{ℎ}$$
3	1 2	ax-mp	$$⊢T\left(0_{ℎ}\right)=0_{ℎ}$$