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 ∈ BndLinOp
Assertion nmbdoplbi ⊢ A ∈ ℋ → norm ℎ ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A

Proof

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