# Metamath Proof Explorer

## 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↔{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↔{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}}↔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↔{T}={0}_{\mathrm{hop}}\right)↔\left({norm}_{\mathrm{op}}\left(if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\right)=0↔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↔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↔{T}={0}_{\mathrm{hop}}\right)$