Metamath Proof Explorer

Theorem nmlno0

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-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}$
Assertion nmlno0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\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 oveq1 ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {U}\mathrm{LnOp}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}$
5 3 4 syl5eq ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {L}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}$
6 5 eleq2d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left({T}\in {L}↔{T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}\right)\right)$
7 oveq1 ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {U}{normOp}_{\mathrm{OLD}}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}$
8 1 7 syl5eq ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {N}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}$
9 8 fveq1d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {N}\left({T}\right)=\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)$
10 9 eqeq1d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left({N}\left({T}\right)=0↔\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0\right)$
11 oveq1 ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {U}{0}_{\mathrm{op}}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}$
12 2 11 syl5eq ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to {Z}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}$
13 12 eqeq2d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left({T}={Z}↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}\right)$
14 10 13 bibi12d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\left({N}\left({T}\right)=0↔{T}={Z}\right)↔\left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}\right)\right)$
15 6 14 imbi12d ${⊢}{U}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\left({T}\in {L}\to \left({N}\left({T}\right)=0↔{T}={Z}\right)\right)↔\left({T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}\right)\to \left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}\right)\right)\right)$
16 oveq2 ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
17 16 eleq2d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left({T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}\right)↔{T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)$
18 oveq2 ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
19 18 fveq1d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\left({T}\right)$
20 19 eqeq1d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0↔\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\left({T}\right)=0\right)$
21 oveq2 ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
22 21 eqeq2d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left({T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
23 20 22 bibi12d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}\right)↔\left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)$
24 17 23 imbi12d ${⊢}{W}=if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\to \left(\left({T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}{W}\right)\to \left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}{W}\right)\right)↔\left({T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\to \left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\right)\right)$
25 eqid ${⊢}if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
26 eqid ${⊢}if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
27 eqid ${⊢}if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)$
28 elimnvu ${⊢}if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\in \mathrm{NrmCVec}$
29 elimnvu ${⊢}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\in \mathrm{NrmCVec}$
30 25 26 27 28 29 nmlno0i ${⊢}{T}\in \left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\mathrm{LnOp}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\to \left(\left(if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){normOp}_{\mathrm{OLD}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)\left({T}\right)=0↔{T}=if\left({U}\in \mathrm{NrmCVec},{U},⟨⟨+,×⟩,\mathrm{abs}⟩\right){0}_{\mathrm{op}}if\left({W}\in \mathrm{NrmCVec},{W},⟨⟨+,×⟩,\mathrm{abs}⟩\right)\right)$
31 15 24 30 dedth2h ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}\to \left({N}\left({T}\right)=0↔{T}={Z}\right)\right)$
32 31 3impia ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({N}\left({T}\right)=0↔{T}={Z}\right)$