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 ffvelrni ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
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ℎ ‘ 𝐴 ) ) )