Theorem nmlnop0

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmlnop0	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ( normop ‘ 𝑇 ) = 0 ↔ ( normop ‘ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ) = 0 ) )
2		eqeq1	⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( 𝑇 = 0hop ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 0hop ) )
3	1 2	bibi12d	⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop ) ↔ ( ( normop ‘ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ) = 0 ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 0hop ) ) )
4		0lnop	⊢ 0hop ∈ LinOp
5	4	elimel	⊢ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ∈ LinOp
6	5	nmlnop0iHIL	⊢ ( ( normop ‘ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ) = 0 ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 0hop )
7	3 6	dedth	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop ) )