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 ⊢normop⁡T=0↔T=0hop

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