Metamath Proof Explorer

Theorem nmbdoplbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmbdoplb.1 
|- T e. BndLinOp
Assertion nmbdoplbi 
|- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

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