# Metamath Proof Explorer

## 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↔{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↔{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}↔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↔{T}={Z}\right)↔\left({N}\left(if\left({T}\in {L},{T},{Z}\right)\right)=0↔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↔if\left({T}\in {L},{T},{Z}\right)={Z}$
21 8 20 dedth ${⊢}{T}\in {L}\to \left({N}\left({T}\right)=0↔{T}={Z}\right)$