Metamath Proof Explorer

Theorem nmlnogt0

Description: The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmlnogt0.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmlnogt0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
nmlnogt0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion nmlnogt0 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ≠ 𝑍 ↔ 0 < ( 𝑁 ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 nmlnogt0.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2 nmlnogt0.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
3 nmlnogt0.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
4 1 2 3 nmlno0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝑇 ) = 0 ↔ 𝑇 = 𝑍 ) )
5 4 necon3bid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ 𝑇 ≠ 𝑍 ) )
6 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
7 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
8 6 7 3 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
9 6 7 1 nmoxr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
10 6 7 1 nmooge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → 0 ≤ ( 𝑁 ‘ 𝑇 ) )
11 0xr ⊢ 0 ∈ ℝ*
12 xrlttri2 ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ ( ( 𝑁 ‘ 𝑇 ) < 0 ∨ 0 < ( 𝑁 ‘ 𝑇 ) ) ) )
13 11 12 mpan2 ⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ ( ( 𝑁 ‘ 𝑇 ) < 0 ∨ 0 < ( 𝑁 ‘ 𝑇 ) ) ) )
14 13 adantr ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝑇 ) ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ ( ( 𝑁 ‘ 𝑇 ) < 0 ∨ 0 < ( 𝑁 ‘ 𝑇 ) ) ) )
15 xrlenlt ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ) → ( 0 ≤ ( 𝑁 ‘ 𝑇 ) ↔ ¬ ( 𝑁 ‘ 𝑇 ) < 0 ) )
16 11 15 mpan ⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* → ( 0 ≤ ( 𝑁 ‘ 𝑇 ) ↔ ¬ ( 𝑁 ‘ 𝑇 ) < 0 ) )
17 16 biimpa ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝑇 ) ) → ¬ ( 𝑁 ‘ 𝑇 ) < 0 )
18 biorf ⊢ ( ¬ ( 𝑁 ‘ 𝑇 ) < 0 → ( 0 < ( 𝑁 ‘ 𝑇 ) ↔ ( ( 𝑁 ‘ 𝑇 ) < 0 ∨ 0 < ( 𝑁 ‘ 𝑇 ) ) ) )
19 17 18 syl ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝑇 ) ) → ( 0 < ( 𝑁 ‘ 𝑇 ) ↔ ( ( 𝑁 ‘ 𝑇 ) < 0 ∨ 0 < ( 𝑁 ‘ 𝑇 ) ) ) )
20 14 19 bitr4d ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* ∧ 0 ≤ ( 𝑁 ‘ 𝑇 ) ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝑇 ) ) )
21 9 10 20 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝑇 ) ) )
22 8 21 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝑇 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝑇 ) ) )
23 5 22 bitr3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ≠ 𝑍 ↔ 0 < ( 𝑁 ‘ 𝑇 ) ) )