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 e. LinOp
Assertion nmlnop0iALT 
|- ( ( normop ` T ) = 0 <-> T = 0hop )

Proof

Step Hyp Ref Expression
1 nmlnop0.1 
 |-  T e. LinOp
2 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
3 2 recnd 
 |-  ( x e. ~H -> ( normh ` x ) e. CC )
4 3 adantr 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` x ) e. CC )
5 norm-i 
 |-  ( x e. ~H -> ( ( normh ` x ) = 0 <-> x = 0h ) )
6 fveq2 
 |-  ( x = 0h -> ( T ` x ) = ( T ` 0h ) )
7 1 lnop0i 
 |-  ( T ` 0h ) = 0h
8 6 7 eqtrdi 
 |-  ( x = 0h -> ( T ` x ) = 0h )
9 5 8 biimtrdi 
 |-  ( x e. ~H -> ( ( normh ` x ) = 0 -> ( T ` x ) = 0h ) )
10 9 necon3d 
 |-  ( x e. ~H -> ( ( T ` x ) =/= 0h -> ( normh ` x ) =/= 0 ) )
11 10 imp 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` x ) =/= 0 )
12 4 11 recne0d 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( 1 / ( normh ` x ) ) =/= 0 )
13 simpr 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( T ` x ) =/= 0h )
14 4 11 reccld 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( 1 / ( normh ` x ) ) e. CC )
15 1 lnopfi 
 |-  T : ~H --> ~H
16 15 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
17 16 adantr 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( T ` x ) e. ~H )
18 hvmul0or 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ ( T ` x ) e. ~H ) -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) = 0h <-> ( ( 1 / ( normh ` x ) ) = 0 \/ ( T ` x ) = 0h ) ) )
19 14 17 18 syl2anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) = 0h <-> ( ( 1 / ( normh ` x ) ) = 0 \/ ( T ` x ) = 0h ) ) )
20 19 necon3abid 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) =/= 0h <-> -. ( ( 1 / ( normh ` x ) ) = 0 \/ ( T ` x ) = 0h ) ) )
21 neanior 
 |-  ( ( ( 1 / ( normh ` x ) ) =/= 0 /\ ( T ` x ) =/= 0h ) <-> -. ( ( 1 / ( normh ` x ) ) = 0 \/ ( T ` x ) = 0h ) )
22 20 21 bitr4di 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) =/= 0h <-> ( ( 1 / ( normh ` x ) ) =/= 0 /\ ( T ` x ) =/= 0h ) ) )
23 12 13 22 mpbir2and 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) =/= 0h )
24 hvmulcl 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ ( T ` x ) e. ~H ) -> ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) e. ~H )
25 14 17 24 syl2anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) e. ~H )
26 normgt0 
 |-  ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) e. ~H -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) =/= 0h <-> 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
27 25 26 syl 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) =/= 0h <-> 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
28 23 27 mpbid 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) )
29 28 ex 
 |-  ( x e. ~H -> ( ( T ` x ) =/= 0h -> 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
30 29 adantl 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( ( T ` x ) =/= 0h -> 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
31 nmopsetretHIL 
 |-  ( T : ~H --> ~H -> { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } C_ RR )
32 15 31 ax-mp 
 |-  { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } C_ RR
33 ressxr 
 |-  RR C_ RR*
34 32 33 sstri 
 |-  { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } C_ RR*
35 simpl 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> x e. ~H )
36 hvmulcl 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ x e. ~H ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. ~H )
37 14 35 36 syl2anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( 1 / ( normh ` x ) ) .h x ) e. ~H )
38 8 necon3i 
 |-  ( ( T ` x ) =/= 0h -> x =/= 0h )
39 norm1 
 |-  ( ( x e. ~H /\ x =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 )
40 38 39 sylan2 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 )
41 1re 
 |-  1 e. RR
42 40 41 eqeltrdi 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) e. RR )
43 eqle 
 |-  ( ( ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) <_ 1 )
44 42 40 43 syl2anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) <_ 1 )
45 1 lnopmuli 
 |-  ( ( ( 1 / ( normh ` x ) ) e. CC /\ x e. ~H ) -> ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) = ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) )
46 14 35 45 syl2anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) = ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) )
47 46 eqcomd 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) = ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) )
48 47 fveq2d 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) ) )
49 fveq2 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( normh ` z ) = ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) )
50 49 breq1d 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( ( normh ` z ) <_ 1 <-> ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) <_ 1 ) )
51 fveq2 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( T ` z ) = ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) )
52 51 fveq2d 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( normh ` ( T ` z ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) ) )
53 52 eqeq2d 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) <-> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) ) ) )
54 50 53 anbi12d 
 |-  ( z = ( ( 1 / ( normh ` x ) ) .h x ) -> ( ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) <-> ( ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) ) ) ) )
55 54 rspcev 
 |-  ( ( ( ( 1 / ( normh ` x ) ) .h x ) e. ~H /\ ( ( normh ` ( ( 1 / ( normh ` x ) ) .h x ) ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` x ) ) .h x ) ) ) ) ) -> E. z e. ~H ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) )
56 37 44 48 55 syl12anc 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> E. z e. ~H ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) )
57 fvex 
 |-  ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. _V
58 eqeq1 
 |-  ( y = ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) -> ( y = ( normh ` ( T ` z ) ) <-> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) )
59 58 anbi2d 
 |-  ( y = ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) -> ( ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) <-> ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) ) )
60 59 rexbidv 
 |-  ( y = ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) -> ( E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) <-> E. z e. ~H ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) ) )
61 57 60 elab 
 |-  ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } <-> E. z e. ~H ( ( normh ` z ) <_ 1 /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) = ( normh ` ( T ` z ) ) ) )
62 56 61 sylibr 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } )
63 supxrub 
 |-  ( ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } C_ RR* /\ ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) )
64 34 62 63 sylancr 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) )
65 64 adantll 
 |-  ( ( ( ( normop ` T ) = 0 /\ x e. ~H ) /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) )
66 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) )
67 15 66 ax-mp 
 |-  ( normop ` T ) = sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < )
68 67 eqeq1i 
 |-  ( ( normop ` T ) = 0 <-> sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) = 0 )
69 68 biimpi 
 |-  ( ( normop ` T ) = 0 -> sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) = 0 )
70 69 ad2antrr 
 |-  ( ( ( ( normop ` T ) = 0 /\ x e. ~H ) /\ ( T ` x ) =/= 0h ) -> sup ( { y | E. z e. ~H ( ( normh ` z ) <_ 1 /\ y = ( normh ` ( T ` z ) ) ) } , RR* , < ) = 0 )
71 65 70 breqtrd 
 |-  ( ( ( ( normop ` T ) = 0 /\ x e. ~H ) /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ 0 )
72 normcl 
 |-  ( ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) e. ~H -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. RR )
73 25 72 syl 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. RR )
74 0re 
 |-  0 e. RR
75 lenlt 
 |-  ( ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) e. RR /\ 0 e. RR ) -> ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ 0 <-> -. 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
76 73 74 75 sylancl 
 |-  ( ( x e. ~H /\ ( T ` x ) =/= 0h ) -> ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ 0 <-> -. 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
77 76 adantll 
 |-  ( ( ( ( normop ` T ) = 0 /\ x e. ~H ) /\ ( T ` x ) =/= 0h ) -> ( ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) <_ 0 <-> -. 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
78 71 77 mpbid 
 |-  ( ( ( ( normop ` T ) = 0 /\ x e. ~H ) /\ ( T ` x ) =/= 0h ) -> -. 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) )
79 78 ex 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( ( T ` x ) =/= 0h -> -. 0 < ( normh ` ( ( 1 / ( normh ` x ) ) .h ( T ` x ) ) ) ) )
80 30 79 pm2.65d 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> -. ( T ` x ) =/= 0h )
81 nne 
 |-  ( -. ( T ` x ) =/= 0h <-> ( T ` x ) = 0h )
82 80 81 sylib 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( T ` x ) = 0h )
83 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
84 83 adantl 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( 0hop ` x ) = 0h )
85 82 84 eqtr4d 
 |-  ( ( ( normop ` T ) = 0 /\ x e. ~H ) -> ( T ` x ) = ( 0hop ` x ) )
86 85 ralrimiva 
 |-  ( ( normop ` T ) = 0 -> A. x e. ~H ( T ` x ) = ( 0hop ` x ) )
87 ffn 
 |-  ( T : ~H --> ~H -> T Fn ~H )
88 15 87 ax-mp 
 |-  T Fn ~H
89 ho0f 
 |-  0hop : ~H --> ~H
90 ffn 
 |-  ( 0hop : ~H --> ~H -> 0hop Fn ~H )
91 89 90 ax-mp 
 |-  0hop Fn ~H
92 eqfnfv 
 |-  ( ( T Fn ~H /\ 0hop Fn ~H ) -> ( T = 0hop <-> A. x e. ~H ( T ` x ) = ( 0hop ` x ) ) )
93 88 91 92 mp2an 
 |-  ( T = 0hop <-> A. x e. ~H ( 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 )