This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )