# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) ) )`
` |-  ( ( ( 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* , < ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) ) ) ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( 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 )`