Theorem lnfn0

Description: The value of a linear Hilbert space functional at zero is zero. Remark in Beran p. 99. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnfn0	$$⊢T\in \mathrm{LinFn}\to T\left(0_{ℎ}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to T\left(0_{ℎ}\right)=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(0_{ℎ}\right)$$
2	1	eqeq1d	$$⊢T=if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\to \left(T\left(0_{ℎ}\right)=0\leftrightarrow if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(0_{ℎ}\right)=0\right)$$
3		0lnfn	$$⊢\mathscr{H}\times \left\{0\right\}\in \mathrm{LinFn}$$
4	3	elimel	$$⊢if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\in \mathrm{LinFn}$$
5	4	lnfn0i	$$⊢if\left(T\in \mathrm{LinFn},T,\mathscr{H}\times \left\{0\right\}\right)\left(0_{ℎ}\right)=0$$
6	2 5	dedth	$$⊢T\in \mathrm{LinFn}\to T\left(0_{ℎ}\right)=0$$