Theorem nmlno0i

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmlno0.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	nmlno0.0	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
	nmlno0.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	nmlno0i.u	⊢ 𝑈 ∈ NrmCVec
	nmlno0i.w	⊢ 𝑊 ∈ NrmCVec
Assertion	nmlno0i	⊢ ( 𝑇 ∈ 𝐿 → ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		nmlno0.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2		nmlno0.0	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
3		nmlno0.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
4		nmlno0i.u	⊢ 𝑈 ∈ NrmCVec
5		nmlno0i.w	⊢ 𝑊 ∈ NrmCVec
6		fveqeq2	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) → ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ ( 𝑁 ‘ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) ) = 0 ) )
7		eqeq1	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) → ( 𝑇 = 𝑍 ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) = 𝑍 ) )
8	6 7	bibi12d	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) → ( ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 ) ↔ ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) ) = 0 ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) = 𝑍 ) ) )
9	2 3	0lno	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ 𝐿 )
10	4 5 9	mp2an	⊢ 𝑍 ∈ 𝐿
11	10	elimel	⊢ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) ∈ 𝐿
12		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
13		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
15		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
16		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
17		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
18		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
19		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
20	1 2 3 4 5 11 12 13 14 15 16 17 18 19	nmlno0lem	⊢ ( ( 𝑁 ‘ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) ) = 0 ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , 𝑍 ) = 𝑍 )
21	8 20	dedth	⊢ ( 𝑇 ∈ 𝐿 → ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 ) )