Metamath Proof Explorer

Theorem nmlno0

Description: The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-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
Assertion nmlno0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ 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 oveq1 ⊢ U = if U ∈ NrmCVec U + × abs → U LnOp W = if U ∈ NrmCVec U + × abs LnOp W
5 3 4 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → L = if U ∈ NrmCVec U + × abs LnOp W
6 5 eleq2d ⊢ U = if U ∈ NrmCVec U + × abs → T ∈ L ↔ T ∈ if U ∈ NrmCVec U + × abs LnOp W
7 oveq1 ⊢ U = if U ∈ NrmCVec U + × abs → U normOp OLD W = if U ∈ NrmCVec U + × abs normOp OLD W
8 1 7 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → N = if U ∈ NrmCVec U + × abs normOp OLD W
9 8 fveq1d ⊢ U = if U ∈ NrmCVec U + × abs → N ⁡ T = if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T
10 9 eqeq1d ⊢ U = if U ∈ NrmCVec U + × abs → N ⁡ T = 0 ↔ if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0
11 oveq1 ⊢ U = if U ∈ NrmCVec U + × abs → U 0 op W = if U ∈ NrmCVec U + × abs 0 op W
12 2 11 eqtrid ⊢ U = if U ∈ NrmCVec U + × abs → Z = if U ∈ NrmCVec U + × abs 0 op W
13 12 eqeq2d ⊢ U = if U ∈ NrmCVec U + × abs → T = Z ↔ T = if U ∈ NrmCVec U + × abs 0 op W
14 10 13 bibi12d ⊢ U = if U ∈ NrmCVec U + × abs → N ⁡ T = 0 ↔ T = Z ↔ if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op W
15 6 14 imbi12d ⊢ U = if U ∈ NrmCVec U + × abs → T ∈ L → N ⁡ T = 0 ↔ T = Z ↔ T ∈ if U ∈ NrmCVec U + × abs LnOp W → if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op W
16 oveq2 ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs LnOp W = if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs
17 16 eleq2d ⊢ W = if W ∈ NrmCVec W + × abs → T ∈ if U ∈ NrmCVec U + × abs LnOp W ↔ T ∈ if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs
18 oveq2 ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD W = if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs
19 18 fveq1d ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ T
20 19 eqeq1d ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0 ↔ if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ T = 0
21 oveq2 ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs 0 op W = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
22 21 eqeq2d ⊢ W = if W ∈ NrmCVec W + × abs → T = if U ∈ NrmCVec U + × abs 0 op W ↔ T = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
23 20 22 bibi12d ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op W ↔ if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
24 17 23 imbi12d ⊢ W = if W ∈ NrmCVec W + × abs → T ∈ if U ∈ NrmCVec U + × abs LnOp W → if U ∈ NrmCVec U + × abs normOp OLD W ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op W ↔ T ∈ if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
25 eqid ⊢ if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs = if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs
26 eqid ⊢ if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
27 eqid ⊢ if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs = if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs
28 elimnvu ⊢ if U ∈ NrmCVec U + × abs ∈ NrmCVec
29 elimnvu ⊢ if W ∈ NrmCVec W + × abs ∈ NrmCVec
30 25 26 27 28 29 nmlno0i ⊢ T ∈ if U ∈ NrmCVec U + × abs LnOp if W ∈ NrmCVec W + × abs → if U ∈ NrmCVec U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ T = 0 ↔ T = if U ∈ NrmCVec U + × abs 0 op if W ∈ NrmCVec W + × abs
31 15 24 30 dedth2h ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → T ∈ L → N ⁡ T = 0 ↔ T = Z
32 31 3impia ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → N ⁡ T = 0 ↔ T = Z