Theorem nmlno0i

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlno0.3	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
	nmlno0.0	$$⊢Z=U{0}_{\mathrm{op}}W$$
	nmlno0.7	$$⊢L=U\mathrm{LnOp}W$$
	nmlno0i.u	$$⊢U\in \mathrm{NrmCVec}$$
	nmlno0i.w	$$⊢W\in \mathrm{NrmCVec}$$
Assertion	nmlno0i	$$⊢T\in L\to \left(N\left(T\right)=0\leftrightarrow T=Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmlno0.3	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
2		nmlno0.0	$$⊢Z=U{0}_{\mathrm{op}}W$$
3		nmlno0.7	$$⊢L=U\mathrm{LnOp}W$$
4		nmlno0i.u	$$⊢U\in \mathrm{NrmCVec}$$
5		nmlno0i.w	$$⊢W\in \mathrm{NrmCVec}$$
6		fveqeq2	$$⊢T=if\left(T\in L,T,Z\right)\to \left(N\left(T\right)=0\leftrightarrow N\left(if\left(T\in L,T,Z\right)\right)=0\right)$$
7		eqeq1	$$⊢T=if\left(T\in L,T,Z\right)\to \left(T=Z\leftrightarrow if\left(T\in L,T,Z\right)=Z\right)$$
8	6 7	bibi12d	$$⊢T=if\left(T\in L,T,Z\right)\to \left(\left(N\left(T\right)=0\leftrightarrow T=Z\right)\leftrightarrow \left(N\left(if\left(T\in L,T,Z\right)\right)=0\leftrightarrow if\left(T\in L,T,Z\right)=Z\right)\right)$$
9	2 3	0lno	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to Z\in L$$
10	4 5 9	mp2an	$$⊢Z\in L$$
11	10	elimel	$$⊢if\left(T\in L,T,Z\right)\in L$$
12		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
13		eqid	$$⊢\mathrm{BaseSet}\left(W\right)=\mathrm{BaseSet}\left(W\right)$$
14		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
15		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(W\right)={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
16		eqid	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(U\right)$$
17		eqid	$$⊢0_{\mathrm{vec}}\left(W\right)=0_{\mathrm{vec}}\left(W\right)$$
18		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
19		eqid	$$⊢{norm}_{CV}\left(W\right)={norm}_{CV}\left(W\right)$$
20	1 2 3 4 5 11 12 13 14 15 16 17 18 19	nmlno0lem	$$⊢N\left(if\left(T\in L,T,Z\right)\right)=0\leftrightarrow if\left(T\in L,T,Z\right)=Z$$
21	8 20	dedth	$$⊢T\in L\to \left(N\left(T\right)=0\leftrightarrow T=Z\right)$$