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 syl6eq
 |-  ( x = 0h -> ( T ` x ) = 0h )
9 5 8 syl6bi
 |-  ( 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 ffvelrni
 |-  ( 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 syl6bbr
 |-  ( ( 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 syl6eq
 |-  ( T = 0hop -> ( normop ` T ) = 0 )
98 94 97 impbii
 |-  ( ( normop ` T ) = 0 <-> T = 0hop )