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	⊢ 𝑇 ∈ LinOp
Assertion	nmlnop0iHIL	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	⊢ 𝑇 ∈ LinOp
2		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3		eqid	⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4	2 3	hhnmoi	⊢ normop = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
5		eqid	⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ 0op ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ 0op ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
6	2 5	hh0oi	⊢ 0hop = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ 0op ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
7		eqid	⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ LnOp ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ LnOp ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
8	2 7	hhlnoi	⊢ LinOp = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ LnOp ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
9	2	hhnv	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
10	4 6 8 9 9	nmlno0i	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop ) )
11	1 10	ax-mp	⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )