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 ⊢ 𝑇 ∈ BndLinOp
Assertion nmbdoplbi ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmbdoplb.1 ⊢ 𝑇 ∈ BndLinOp
2 fveq2 ⊢ ( 𝐴 = 0ℎ → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ 0ℎ ) )
3 2 fveq2d ⊢ ( 𝐴 = 0ℎ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) = ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) )
4 fveq2 ⊢ ( 𝐴 = 0ℎ → ( normℎ ‘ 𝐴 ) = ( normℎ ‘ 0ℎ ) )
5 4 oveq2d ⊢ ( 𝐴 = 0ℎ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) ) )
6 3 5 breq12d ⊢ ( 𝐴 = 0ℎ → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) ) ) )
7 bdopln ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
8 1 7 ax-mp ⊢ 𝑇 ∈ LinOp
9 8 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
10 9 ffvelrni ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
11 normcl ⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
12 10 11 syl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℂ )
15 normcl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ 𝐴 ) ∈ ℝ )
17 16 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ 𝐴 ) ∈ ℂ )
18 normne0 ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0ℎ ) )
19 18 biimpar ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ 𝐴 ) ≠ 0 )
20 14 17 19 divrec2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
21 16 19 rereccld ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ )
23 simpl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 𝐴 ∈ ℋ )
24 8 lnopmuli ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ ( 𝑇 ‘ 𝐴 ) ) )
25 22 23 24 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ ( 𝑇 ‘ 𝐴 ) ) )
26 25 fveq2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) = ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) )
27 10 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
28 norm-iii ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝐴 ) ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
29 22 27 28 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
30 normgt0 ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
31 30 biimpa ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( normℎ ‘ 𝐴 ) )
32 16 31 recgt0d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) )
33 0re ⊢ 0 ∈ ℝ
34 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
35 33 34 mpan ⊢ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
36 21 32 35 sylc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) )
37 21 36 absidd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) = ( 1 / ( normℎ ‘ 𝐴 ) ) )
38 37 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
39 26 29 38 3eqtrrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
40 20 39 eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
41 hvmulcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
42 22 23 41 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
43 normcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
44 42 43 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
45 norm1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 )
46 eqle ⊢ ( ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
47 44 45 46 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
48 nmoplb ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normop ‘ 𝑇 ) )
49 9 48 mp3an1 ⊢ ( ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normop ‘ 𝑇 ) )
50 42 47 49 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normop ‘ 𝑇 ) )
51 40 50 eqbrtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normop ‘ 𝑇 ) )
52 nmopre ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
53 1 52 ax-mp ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
54 53 a1i ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normop ‘ 𝑇 ) ∈ ℝ )
55 ledivmul2 ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( normℎ ‘ 𝐴 ) ) ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normop ‘ 𝑇 ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
56 13 54 16 31 55 syl112anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normop ‘ 𝑇 ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
57 51 56 mpbid ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
58 0le0 ⊢ 0 ≤ 0
59 8 lnop0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0ℎ
60 59 fveq2i ⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = ( normℎ ‘ 0ℎ )
61 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
62 60 61 eqtri ⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) = 0
63 61 oveq2i ⊢ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) ) = ( ( normop ‘ 𝑇 ) · 0 )
64 53 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
65 64 mul01i ⊢ ( ( normop ‘ 𝑇 ) · 0 ) = 0
66 63 65 eqtri ⊢ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) ) = 0
67 58 62 66 3brtr4i ⊢ ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) )
68 67 a1i ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 0ℎ ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 0ℎ ) ) )
69 6 57 68 pm2.61ne ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )