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 ⊢ N = U normOp OLD W
nmlnogt0.0 ⊢ Z = U 0 op W
nmlnogt0.7 ⊢ L = U LnOp W
Assertion nmlnogt0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ≠ Z ↔ 0 < N ⁡ T

Proof

Step Hyp Ref Expression
1 nmlnogt0.3 ⊢ N = U normOp OLD W
2 nmlnogt0.0 ⊢ Z = U 0 op W
3 nmlnogt0.7 ⊢ L = U LnOp W
4 1 2 3 nmlno0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → N ⁡ T = 0 ↔ T = Z
5 4 necon3bid ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → N ⁡ T ≠ 0 ↔ T ≠ Z
6 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
7 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
8 6 7 3 lnof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T : BaseSet ⁡ U ⟶ BaseSet ⁡ W
9 6 7 1 nmoxr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : BaseSet ⁡ U ⟶ BaseSet ⁡ W → N ⁡ T ∈ ℝ *
10 6 7 1 nmooge0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : BaseSet ⁡ U ⟶ BaseSet ⁡ W → 0 ≤ N ⁡ T
11 0xr ⊢ 0 ∈ ℝ *
12 xrlttri2 ⊢ N ⁡ T ∈ ℝ * ∧ 0 ∈ ℝ * → N ⁡ T ≠ 0 ↔ N ⁡ T < 0 ∨ 0 < N ⁡ T
13 11 12 mpan2 ⊢ N ⁡ T ∈ ℝ * → N ⁡ T ≠ 0 ↔ N ⁡ T < 0 ∨ 0 < N ⁡ T
14 13 adantr ⊢ N ⁡ T ∈ ℝ * ∧ 0 ≤ N ⁡ T → N ⁡ T ≠ 0 ↔ N ⁡ T < 0 ∨ 0 < N ⁡ T
15 xrlenlt ⊢ 0 ∈ ℝ * ∧ N ⁡ T ∈ ℝ * → 0 ≤ N ⁡ T ↔ ¬ N ⁡ T < 0
16 11 15 mpan ⊢ N ⁡ T ∈ ℝ * → 0 ≤ N ⁡ T ↔ ¬ N ⁡ T < 0
17 16 biimpa ⊢ N ⁡ T ∈ ℝ * ∧ 0 ≤ N ⁡ T → ¬ N ⁡ T < 0
18 biorf ⊢ ¬ N ⁡ T < 0 → 0 < N ⁡ T ↔ N ⁡ T < 0 ∨ 0 < N ⁡ T
19 17 18 syl ⊢ N ⁡ T ∈ ℝ * ∧ 0 ≤ N ⁡ T → 0 < N ⁡ T ↔ N ⁡ T < 0 ∨ 0 < N ⁡ T
20 14 19 bitr4d ⊢ N ⁡ T ∈ ℝ * ∧ 0 ≤ N ⁡ T → N ⁡ T ≠ 0 ↔ 0 < N ⁡ T
21 9 10 20 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : BaseSet ⁡ U ⟶ BaseSet ⁡ W → N ⁡ T ≠ 0 ↔ 0 < N ⁡ T
22 8 21 syld3an3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → N ⁡ T ≠ 0 ↔ 0 < N ⁡ T
23 5 22 bitr3d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ≠ Z ↔ 0 < N ⁡ T