This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmcoplbi

Description: A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcopex.1 
|- T e. LinOp
nmcopex.2 
|- T e. ContOp
Assertion nmcoplbi 
|- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmcopex.1 
 |-  T e. LinOp
2 nmcopex.2 
 |-  T e. ContOp
3 0le0 
 |-  0 <_ 0
4 3 a1i 
 |-  ( A = 0h -> 0 <_ 0 )
5 fveq2 
 |-  ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
6 1 lnop0i 
 |-  ( T ` 0h ) = 0h
7 5 6 eqtrdi 
 |-  ( A = 0h -> ( T ` A ) = 0h )
8 7 fveq2d 
 |-  ( A = 0h -> ( normh ` ( T ` A ) ) = ( normh ` 0h ) )
9 norm0 
 |-  ( normh ` 0h ) = 0
10 8 9 eqtrdi 
 |-  ( A = 0h -> ( normh ` ( T ` A ) ) = 0 )
11 fveq2 
 |-  ( A = 0h -> ( normh ` A ) = ( normh ` 0h ) )
12 11 9 eqtrdi 
 |-  ( A = 0h -> ( normh ` A ) = 0 )
13 12 oveq2d 
 |-  ( A = 0h -> ( ( normop ` T ) x. ( normh ` A ) ) = ( ( normop ` T ) x. 0 ) )
14 1 2 nmcopexi 
 |-  ( normop ` T ) e. RR
15 14 recni 
 |-  ( normop ` T ) e. CC
16 15 mul01i 
 |-  ( ( normop ` T ) x. 0 ) = 0
17 13 16 eqtrdi 
 |-  ( A = 0h -> ( ( normop ` T ) x. ( normh ` A ) ) = 0 )
18 4 10 17 3brtr4d 
 |-  ( A = 0h -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
19 18 adantl 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
20 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
21 20 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. RR )
22 normne0 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
23 22 biimpar 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) =/= 0 )
24 21 23 rereccld 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
25 normgt0 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
26 25 biimpa 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( normh ` A ) )
27 21 26 recgt0d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
28 0re 
 |-  0 e. RR
29 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
30 28 29 mpan 
 |-  ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
31 24 27 30 sylc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
32 24 31 absidd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
33 32 oveq1d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( normh ` ( T ` A ) ) ) )
34 24 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
35 simpl 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> A e. ~H )
36 1 lnopmuli 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) )
37 34 35 36 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) )
38 37 fveq2d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) )
39 1 lnopfi 
 |-  T : ~H --> ~H
40 39 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. ~H )
41 40 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( T ` A ) e. ~H )
42 norm-iii 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ ( T ` A ) e. ~H ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
43 34 41 42 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
44 38 43 eqtrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
45 normcl 
 |-  ( ( T ` A ) e. ~H -> ( normh ` ( T ` A ) ) e. RR )
46 40 45 syl 
 |-  ( A e. ~H -> ( normh ` ( T ` A ) ) e. RR )
47 46 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) e. RR )
48 47 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) e. CC )
49 21 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. CC )
50 48 49 23 divrec2d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( normh ` ( T ` A ) ) ) )
51 33 44 50 3eqtr4rd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
52 hvmulcl 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
53 34 35 52 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
54 normcl 
 |-  ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
55 53 54 syl 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
56 norm1 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
57 eqle 
 |-  ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
58 55 56 57 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
59 nmoplb 
 |-  ( ( T : ~H --> ~H /\ ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
60 39 59 mp3an1 
 |-  ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
61 53 58 60 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
62 51 61 eqbrtrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) )
63 14 a1i 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normop ` T ) e. RR )
64 ledivmul2 
 |-  ( ( ( normh ` ( T ` A ) ) e. RR /\ ( normop ` T ) e. RR /\ ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) ) -> ( ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) <-> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
65 47 63 21 26 64 syl112anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) <-> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
66 62 65 mpbid 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
67 19 66 pm2.61dane 
 |-  ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )