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

Proof

Step Hyp Ref Expression
1 nmlno0.3 ⊢ N = U normOp OLD W
2 nmlno0.0 ⊢ Z = U 0 op W
3 nmlno0.7 ⊢ L = U LnOp W
4 nmlno0i.u ⊢ U ∈ NrmCVec
5 nmlno0i.w ⊢ W ∈ NrmCVec
6 fveqeq2 ⊢ T = if T ∈ L T Z → N ⁡ T = 0 ↔ N ⁡ if T ∈ L T Z = 0
7 eqeq1 ⊢ T = if T ∈ L T Z → T = Z ↔ if T ∈ L T Z = Z
8 6 7 bibi12d ⊢ T = if T ∈ L T Z → N ⁡ T = 0 ↔ T = Z ↔ N ⁡ if T ∈ L T Z = 0 ↔ if T ∈ L T Z = Z
9 2 3 0lno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ L
10 4 5 9 mp2an ⊢ Z ∈ L
11 10 elimel ⊢ if T ∈ L T Z ∈ L
12 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
13 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
14 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
15 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
16 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
17 eqid ⊢ 0 vec ⁡ W = 0 vec ⁡ W
18 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
19 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
20 1 2 3 4 5 11 12 13 14 15 16 17 18 19 nmlno0lem ⊢ N ⁡ if T ∈ L T Z = 0 ↔ if T ∈ L T Z = Z
21 8 20 dedth ⊢ T ∈ L → N ⁡ T = 0 ↔ T = Z