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