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

Metamath Proof Explorer

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 ↔ 𝑇 = 𝑍 ) )