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 โŠข ๐‘‡ โˆˆ LinOp
nmcopex.2 โŠข ๐‘‡ โˆˆ ContOp
Assertion nmcoplbi ( ๐ด โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 nmcopex.1 โŠข ๐‘‡ โˆˆ LinOp
2 nmcopex.2 โŠข ๐‘‡ โˆˆ ContOp
3 0le0 โŠข 0 โ‰ค 0
4 3 a1i โŠข ( ๐ด = 0โ„Ž โ†’ 0 โ‰ค 0 )
5 fveq2 โŠข ( ๐ด = 0โ„Ž โ†’ ( ๐‘‡ โ€˜ ๐ด ) = ( ๐‘‡ โ€˜ 0โ„Ž ) )
6 1 lnop0i โŠข ( ๐‘‡ โ€˜ 0โ„Ž ) = 0โ„Ž
7 5 6 eqtrdi โŠข ( ๐ด = 0โ„Ž โ†’ ( ๐‘‡ โ€˜ ๐ด ) = 0โ„Ž )
8 7 fveq2d โŠข ( ๐ด = 0โ„Ž โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) = ( normโ„Ž โ€˜ 0โ„Ž ) )
9 norm0 โŠข ( normโ„Ž โ€˜ 0โ„Ž ) = 0
10 8 9 eqtrdi โŠข ( ๐ด = 0โ„Ž โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) = 0 )
11 fveq2 โŠข ( ๐ด = 0โ„Ž โ†’ ( normโ„Ž โ€˜ ๐ด ) = ( normโ„Ž โ€˜ 0โ„Ž ) )
12 11 9 eqtrdi โŠข ( ๐ด = 0โ„Ž โ†’ ( normโ„Ž โ€˜ ๐ด ) = 0 )
13 12 oveq2d โŠข ( ๐ด = 0โ„Ž โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) = ( ( normop โ€˜ ๐‘‡ ) ยท 0 ) )
14 1 2 nmcopexi โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„
15 14 recni โŠข ( normop โ€˜ ๐‘‡ ) โˆˆ โ„‚
16 15 mul01i โŠข ( ( normop โ€˜ ๐‘‡ ) ยท 0 ) = 0
17 13 16 eqtrdi โŠข ( ๐ด = 0โ„Ž โ†’ ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) = 0 )
18 4 10 17 3brtr4d โŠข ( ๐ด = 0โ„Ž โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) )
19 18 adantl โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด = 0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) )
20 normcl โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ๐ด ) โˆˆ โ„ )
21 20 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ๐ด ) โˆˆ โ„ )
22 normne0 โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ๐ด ) โ‰  0 โ†” ๐ด โ‰  0โ„Ž ) )
23 22 biimpar โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ๐ด ) โ‰  0 )
24 21 23 rereccld โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„ )
25 normgt0 โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐ด โ‰  0โ„Ž โ†” 0 < ( normโ„Ž โ€˜ ๐ด ) ) )
26 25 biimpa โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ 0 < ( normโ„Ž โ€˜ ๐ด ) )
27 21 26 recgt0d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ 0 < ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) )
28 0re โŠข 0 โˆˆ โ„
29 ltle โŠข ( ( 0 โˆˆ โ„ โˆง ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„ ) โ†’ ( 0 < ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โ†’ 0 โ‰ค ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) )
30 28 29 mpan โŠข ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„ โ†’ ( 0 < ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โ†’ 0 โ‰ค ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) )
31 24 27 30 sylc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ 0 โ‰ค ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) )
32 24 31 absidd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( abs โ€˜ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) = ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) )
33 32 oveq1d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( abs โ€˜ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) = ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) )
34 24 recnd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„‚ )
35 simpl โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ๐ด โˆˆ โ„‹ )
36 1 lnopmuli โŠข ( ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) = ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐ด ) ) )
37 34 35 36 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) = ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐ด ) ) )
38 37 fveq2d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) = ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐ด ) ) ) )
39 1 lnopfi โŠข ๐‘‡ : โ„‹ โŸถ โ„‹
40 39 ffvelcdmi โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( ๐‘‡ โ€˜ ๐ด ) โˆˆ โ„‹ )
41 40 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ๐‘‡ โ€˜ ๐ด ) โˆˆ โ„‹ )
42 norm-iii โŠข ( ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐ด ) โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐ด ) ) ) = ( ( abs โ€˜ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) )
43 34 41 42 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐ด ) ) ) = ( ( abs โ€˜ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) )
44 38 43 eqtrd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) = ( ( abs โ€˜ ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) )
45 normcl โŠข ( ( ๐‘‡ โ€˜ ๐ด ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โˆˆ โ„ )
46 40 45 syl โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โˆˆ โ„ )
47 46 adantr โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โˆˆ โ„ )
48 47 recnd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โˆˆ โ„‚ )
49 21 recnd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ๐ด ) โˆˆ โ„‚ )
50 48 49 23 divrec2d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) / ( normโ„Ž โ€˜ ๐ด ) ) = ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยท ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) ) )
51 33 44 50 3eqtr4rd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) / ( normโ„Ž โ€˜ ๐ด ) ) = ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) )
52 hvmulcl โŠข ( ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) โˆˆ โ„‹ )
53 34 35 52 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) โˆˆ โ„‹ )
54 normcl โŠข ( ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โˆˆ โ„ )
55 53 54 syl โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โˆˆ โ„ )
56 norm1 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) = 1 )
57 eqle โŠข ( ( ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โˆˆ โ„ โˆง ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) = 1 ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โ‰ค 1 )
58 55 56 57 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โ‰ค 1 )
59 nmoplb โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
60 39 59 mp3an1 โŠข ( ( ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) โ‰ค 1 ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
61 53 58 60 syl2anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ( ( 1 / ( normโ„Ž โ€˜ ๐ด ) ) ยทโ„Ž ๐ด ) ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
62 51 61 eqbrtrd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) / ( normโ„Ž โ€˜ ๐ด ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) )
63 14 a1i โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ )
64 ledivmul2 โŠข ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โˆˆ โ„ โˆง ( normop โ€˜ ๐‘‡ ) โˆˆ โ„ โˆง ( ( normโ„Ž โ€˜ ๐ด ) โˆˆ โ„ โˆง 0 < ( normโ„Ž โ€˜ ๐ด ) ) ) โ†’ ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) / ( normโ„Ž โ€˜ ๐ด ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) โ†” ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) ) )
65 47 63 21 26 64 syl112anc โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) / ( normโ„Ž โ€˜ ๐ด ) ) โ‰ค ( normop โ€˜ ๐‘‡ ) โ†” ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) ) )
66 62 65 mpbid โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ด โ‰  0โ„Ž ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) )
67 19 66 pm2.61dane โŠข ( ๐ด โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐ด ) ) โ‰ค ( ( normop โ€˜ ๐‘‡ ) ยท ( normโ„Ž โ€˜ ๐ด ) ) )