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 LinOp$
	Assertion	nmlnop0iHIL	$⊢ {norm}_{op} (T) = 0 \leftrightarrow T = 0_{hop}$

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

Metamath Proof Explorer