Metamath Proof Explorer


Theorem nmlnop0iALT

Description: A linear operator with a zero norm is identically zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis nmlnop0.1 𝑇 ∈ LinOp
Assertion nmlnop0iALT ( ( normop𝑇 ) = 0 ↔ 𝑇 = 0hop )

Proof

Step Hyp Ref Expression
1 nmlnop0.1 𝑇 ∈ LinOp
2 normcl ( 𝑥 ∈ ℋ → ( norm𝑥 ) ∈ ℝ )
3 2 recnd ( 𝑥 ∈ ℋ → ( norm𝑥 ) ∈ ℂ )
4 3 adantr ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm𝑥 ) ∈ ℂ )
5 norm-i ( 𝑥 ∈ ℋ → ( ( norm𝑥 ) = 0 ↔ 𝑥 = 0 ) )
6 fveq2 ( 𝑥 = 0 → ( 𝑇𝑥 ) = ( 𝑇 ‘ 0 ) )
7 1 lnop0i ( 𝑇 ‘ 0 ) = 0
8 6 7 eqtrdi ( 𝑥 = 0 → ( 𝑇𝑥 ) = 0 )
9 5 8 syl6bi ( 𝑥 ∈ ℋ → ( ( norm𝑥 ) = 0 → ( 𝑇𝑥 ) = 0 ) )
10 9 necon3d ( 𝑥 ∈ ℋ → ( ( 𝑇𝑥 ) ≠ 0 → ( norm𝑥 ) ≠ 0 ) )
11 10 imp ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm𝑥 ) ≠ 0 )
12 4 11 recne0d ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( 1 / ( norm𝑥 ) ) ≠ 0 )
13 simpr ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( 𝑇𝑥 ) ≠ 0 )
14 4 11 reccld ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( 1 / ( norm𝑥 ) ) ∈ ℂ )
15 1 lnopfi 𝑇 : ℋ ⟶ ℋ
16 15 ffvelrni ( 𝑥 ∈ ℋ → ( 𝑇𝑥 ) ∈ ℋ )
17 16 adantr ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( 𝑇𝑥 ) ∈ ℋ )
18 hvmul0or ( ( ( 1 / ( norm𝑥 ) ) ∈ ℂ ∧ ( 𝑇𝑥 ) ∈ ℋ ) → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) = 0 ↔ ( ( 1 / ( norm𝑥 ) ) = 0 ∨ ( 𝑇𝑥 ) = 0 ) ) )
19 14 17 18 syl2anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) = 0 ↔ ( ( 1 / ( norm𝑥 ) ) = 0 ∨ ( 𝑇𝑥 ) = 0 ) ) )
20 19 necon3abid ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ≠ 0 ↔ ¬ ( ( 1 / ( norm𝑥 ) ) = 0 ∨ ( 𝑇𝑥 ) = 0 ) ) )
21 neanior ( ( ( 1 / ( norm𝑥 ) ) ≠ 0 ∧ ( 𝑇𝑥 ) ≠ 0 ) ↔ ¬ ( ( 1 / ( norm𝑥 ) ) = 0 ∨ ( 𝑇𝑥 ) = 0 ) )
22 20 21 bitr4di ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ≠ 0 ↔ ( ( 1 / ( norm𝑥 ) ) ≠ 0 ∧ ( 𝑇𝑥 ) ≠ 0 ) ) )
23 12 13 22 mpbir2and ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ≠ 0 )
24 hvmulcl ( ( ( 1 / ( norm𝑥 ) ) ∈ ℂ ∧ ( 𝑇𝑥 ) ∈ ℋ ) → ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ∈ ℋ )
25 14 17 24 syl2anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ∈ ℋ )
26 normgt0 ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ∈ ℋ → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ≠ 0 ↔ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
27 25 26 syl ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ≠ 0 ↔ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
28 23 27 mpbid ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) )
29 28 ex ( 𝑥 ∈ ℋ → ( ( 𝑇𝑥 ) ≠ 0 → 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
30 29 adantl ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇𝑥 ) ≠ 0 → 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
31 nmopsetretHIL ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ⊆ ℝ )
32 15 31 ax-mp { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ⊆ ℝ
33 ressxr ℝ ⊆ ℝ*
34 32 33 sstri { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ⊆ ℝ*
35 simpl ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → 𝑥 ∈ ℋ )
36 hvmulcl ( ( ( 1 / ( norm𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ∈ ℋ )
37 14 35 36 syl2anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ∈ ℋ )
38 8 necon3i ( ( 𝑇𝑥 ) ≠ 0𝑥 ≠ 0 )
39 norm1 ( ( 𝑥 ∈ ℋ ∧ 𝑥 ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) = 1 )
40 38 39 sylan2 ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) = 1 )
41 1re 1 ∈ ℝ
42 40 41 eqeltrdi ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ∈ ℝ )
43 eqle ( ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ∈ ℝ ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) = 1 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ≤ 1 )
44 42 40 43 syl2anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ≤ 1 )
45 1 lnopmuli ( ( ( 1 / ( norm𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) = ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) )
46 14 35 45 syl2anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) = ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) )
47 46 eqcomd ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) = ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) )
48 47 fveq2d ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ) )
49 fveq2 ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( norm𝑧 ) = ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) )
50 49 breq1d ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( ( norm𝑧 ) ≤ 1 ↔ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ≤ 1 ) )
51 fveq2 ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( 𝑇𝑧 ) = ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) )
52 51 fveq2d ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( norm ‘ ( 𝑇𝑧 ) ) = ( norm ‘ ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ) )
53 52 eqeq2d ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ↔ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ) ) )
54 50 53 anbi12d ( 𝑧 = ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) → ( ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) ↔ ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ) ) ) )
55 54 rspcev ( ( ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ∈ ℋ ∧ ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇 ‘ ( ( 1 / ( norm𝑥 ) ) · 𝑥 ) ) ) ) ) → ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) )
56 37 44 48 55 syl12anc ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) )
57 fvex ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ V
58 eqeq1 ( 𝑦 = ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) → ( 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ↔ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) )
59 58 anbi2d ( 𝑦 = ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) → ( ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) ↔ ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) ) )
60 59 rexbidv ( 𝑦 = ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) → ( ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) ↔ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) ) )
61 57 60 elab ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ↔ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) = ( norm ‘ ( 𝑇𝑧 ) ) ) )
62 56 61 sylibr ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } )
63 supxrub ( ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ⊆ ℝ* ∧ ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) )
64 34 62 63 sylancr ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) )
65 64 adantll ( ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) )
66 nmopval ( 𝑇 : ℋ ⟶ ℋ → ( normop𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) )
67 15 66 ax-mp ( normop𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < )
68 67 eqeq1i ( ( normop𝑇 ) = 0 ↔ sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) = 0 )
69 68 biimpi ( ( normop𝑇 ) = 0 → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) = 0 )
70 69 ad2antrr ( ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇𝑥 ) ≠ 0 ) → sup ( { 𝑦 ∣ ∃ 𝑧 ∈ ℋ ( ( norm𝑧 ) ≤ 1 ∧ 𝑦 = ( norm ‘ ( 𝑇𝑧 ) ) ) } , ℝ* , < ) = 0 )
71 65 70 breqtrd ( ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ 0 )
72 normcl ( ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ∈ ℋ → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ ℝ )
73 25 72 syl ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ ℝ )
74 0re 0 ∈ ℝ
75 lenlt ( ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
76 73 74 75 sylancl ( ( 𝑥 ∈ ℋ ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
77 76 adantll ( ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇𝑥 ) ≠ 0 ) → ( ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ≤ 0 ↔ ¬ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
78 71 77 mpbid ( ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇𝑥 ) ≠ 0 ) → ¬ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) )
79 78 ex ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇𝑥 ) ≠ 0 → ¬ 0 < ( norm ‘ ( ( 1 / ( norm𝑥 ) ) · ( 𝑇𝑥 ) ) ) ) )
80 30 79 pm2.65d ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ¬ ( 𝑇𝑥 ) ≠ 0 )
81 nne ( ¬ ( 𝑇𝑥 ) ≠ 0 ↔ ( 𝑇𝑥 ) = 0 )
82 80 81 sylib ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑇𝑥 ) = 0 )
83 ho0val ( 𝑥 ∈ ℋ → ( 0hop𝑥 ) = 0 )
84 83 adantl ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 0hop𝑥 ) = 0 )
85 82 84 eqtr4d ( ( ( normop𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑇𝑥 ) = ( 0hop𝑥 ) )
86 85 ralrimiva ( ( normop𝑇 ) = 0 → ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 0hop𝑥 ) )
87 ffn ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
88 15 87 ax-mp 𝑇 Fn ℋ
89 ho0f 0hop : ℋ ⟶ ℋ
90 ffn ( 0hop : ℋ ⟶ ℋ → 0hop Fn ℋ )
91 89 90 ax-mp 0hop Fn ℋ
92 eqfnfv ( ( 𝑇 Fn ℋ ∧ 0hop Fn ℋ ) → ( 𝑇 = 0hop ↔ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 0hop𝑥 ) ) )
93 88 91 92 mp2an ( 𝑇 = 0hop ↔ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 0hop𝑥 ) )
94 86 93 sylibr ( ( normop𝑇 ) = 0 → 𝑇 = 0hop )
95 fveq2 ( 𝑇 = 0hop → ( normop𝑇 ) = ( normop ‘ 0hop ) )
96 nmop0 ( normop ‘ 0hop ) = 0
97 95 96 eqtrdi ( 𝑇 = 0hop → ( normop𝑇 ) = 0 )
98 94 97 impbii ( ( normop𝑇 ) = 0 ↔ 𝑇 = 0hop )