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 ∈ LinOp
nmcopex.2 ⊢ T ∈ ContOp
Assertion nmcoplbi ⊢ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 nmcopex.1 ⊢ T ∈ LinOp
2 nmcopex.2 ⊢ T ∈ ContOp
3 0le0 ⊢ 0 ≤ 0
4 3 a1i ⊢ A = 0 ℎ → 0 ≤ 0
5 fveq2 ⊢ A = 0 ℎ → T ⁡ A = T ⁡ 0 ℎ
6 1 lnop0i ⊢ T ⁡ 0 ℎ = 0 ℎ
7 5 6 eqtrdi ⊢ A = 0 ℎ → T ⁡ A = 0 ℎ
8 7 fveq2d ⊢ A = 0 ℎ → norm ℎ ⁡ T ⁡ A = norm ℎ ⁡ 0 ℎ
9 norm0 ⊢ norm ℎ ⁡ 0 ℎ = 0
10 8 9 eqtrdi ⊢ A = 0 ℎ → norm ℎ ⁡ T ⁡ A = 0
11 fveq2 ⊢ A = 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ 0 ℎ
12 11 9 eqtrdi ⊢ A = 0 ℎ → norm ℎ ⁡ A = 0
13 12 oveq2d ⊢ A = 0 ℎ → norm op ⁡ T ⁢ norm ℎ ⁡ A = norm op ⁡ T ⋅ 0
14 1 2 nmcopexi ⊢ norm op ⁡ T ∈ ℝ
15 14 recni ⊢ norm op ⁡ T ∈ ℂ
16 15 mul01i ⊢ norm op ⁡ T ⋅ 0 = 0
17 13 16 eqtrdi ⊢ A = 0 ℎ → norm op ⁡ T ⁢ norm ℎ ⁡ A = 0
18 4 10 17 3brtr4d ⊢ A = 0 ℎ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
19 18 adantl ⊢ A ∈ ℋ ∧ A = 0 ℎ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
20 normcl ⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ
21 20 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℝ
22 normne0 ⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ
23 22 biimpar ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ≠ 0
24 21 23 rereccld ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℝ
25 normgt0 ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A
26 25 biimpa ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < norm ℎ ⁡ A
27 21 26 recgt0d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < 1 norm ℎ ⁡ A
28 0re ⊢ 0 ∈ ℝ
29 ltle ⊢ 0 ∈ ℝ ∧ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
30 28 29 mpan ⊢ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
31 24 27 30 sylc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A
32 24 31 absidd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A = 1 norm ℎ ⁡ A
33 32 oveq1d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A
34 24 recnd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℂ
35 simpl ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ ℋ
36 1 lnopmuli ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⋅ ℎ T ⁡ A
37 34 35 36 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⋅ ℎ T ⁡ A
38 37 fveq2d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ T ⁡ A
39 1 lnopfi ⊢ T : ℋ ⟶ ℋ
40 39 ffvelrni ⊢ A ∈ ℋ → T ⁡ A ∈ ℋ
41 40 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ∈ ℋ
42 norm-iii ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ T ⁡ A ∈ ℋ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ T ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A
43 34 41 42 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ T ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A
44 38 43 eqtrd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A
45 normcl ⊢ T ⁡ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ∈ ℝ
46 40 45 syl ⊢ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ∈ ℝ
47 46 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A ∈ ℝ
48 47 recnd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A ∈ ℂ
49 21 recnd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℂ
50 48 49 23 divrec2d ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ norm ℎ ⁡ T ⁡ A
51 33 44 50 3eqtr4rd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A norm ℎ ⁡ A = norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A
52 hvmulcl ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ
53 34 35 52 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ
54 normcl ⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ
55 53 54 syl ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ
56 norm1 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1
57 eqle ⊢ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1
58 55 56 57 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1
59 nmoplb ⊢ T : ℋ ⟶ ℋ ∧ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm op ⁡ T
60 39 59 mp3an1 ⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm op ⁡ T
61 53 58 60 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm op ⁡ T
62 51 61 eqbrtrd ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A norm ℎ ⁡ A ≤ norm op ⁡ T
63 14 a1i ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm op ⁡ T ∈ ℝ
64 ledivmul2 ⊢ norm ℎ ⁡ T ⁡ A ∈ ℝ ∧ norm op ⁡ T ∈ ℝ ∧ norm ℎ ⁡ A ∈ ℝ ∧ 0 < norm ℎ ⁡ A → norm ℎ ⁡ T ⁡ A norm ℎ ⁡ A ≤ norm op ⁡ T ↔ norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
65 47 63 21 26 64 syl112anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A norm ℎ ⁡ A ≤ norm op ⁡ T ↔ norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
66 62 65 mpbid ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
67 19 66 pm2.61dane ⊢ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A