Theorem nmlnop0

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmlnop0	$$⊢T\in \mathrm{LinOp}\to \left({norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢T=if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\to \left({norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow {norm}_{\mathrm{op}}\left(if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\right)=0\right)$$
2		eqeq1	$$⊢T=if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\to \left(T=0_{\mathrm{hop}}\leftrightarrow if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}\right)$$
3	1 2	bibi12d	$$⊢T=if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\to \left(\left({norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}\right)\leftrightarrow \left({norm}_{\mathrm{op}}\left(if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\right)=0\leftrightarrow if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}\right)\right)$$
4		0lnop	$$⊢0_{\mathrm{hop}}\in \mathrm{LinOp}$$
5	4	elimel	$$⊢if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\in \mathrm{LinOp}$$
6	5	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)\right)=0\leftrightarrow if\left(T\in \mathrm{LinOp},T,0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}$$
7	3 6	dedth	$$⊢T\in \mathrm{LinOp}\to \left({norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}\right)$$