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 biimtrdi ⊢ ( 𝑥 ∈ ℋ → ( ( 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 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 )