Theorem nmlnop0iHIL

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 18-Jan-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	$$⊢T\in \mathrm{LinOp}$$
2		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
3		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
4	2 3	hhnmoi	$$⊢{norm}_{\mathrm{op}}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
5		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩0_{\mathrm{op}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩0_{\mathrm{op}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
6	2 5	hh0oi	$$⊢0_{\mathrm{hop}}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩0_{\mathrm{op}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
7		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
8	2 7	hhlnoi	$$⊢\mathrm{LinOp}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\mathrm{LnOp}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
9	2	hhnv	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
10	4 6 8 9 9	nmlno0i	$$⊢T\in \mathrm{LinOp}\to \left({norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}\right)$$
11	1 10	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$