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 ⊢ T ∈ LinOp
Assertion nmlnop0iALT ⊢ norm op ⁡ T = 0 ↔ T = 0 hop

Proof

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