Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  cnlnadjlem7 Structured version   Visualization version   GIF version

 Description: Lemma for cnlnadji 29269. Helper lemma to show that 𝐹 is continuous. (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
cnlnadjlem.4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
cnlnadjlem.5 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
Assertion
Ref Expression
cnlnadjlem7 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))
Distinct variable groups:   𝑣,𝑔,𝑤,𝑦,𝐴   𝑤,𝐹   𝑇,𝑔,𝑣,𝑤,𝑦   𝑣,𝐺,𝑤
Allowed substitution hints:   𝐵(𝑦,𝑤,𝑣,𝑔)   𝐹(𝑦,𝑣,𝑔)   𝐺(𝑦,𝑔)

StepHypRef Expression
1 breq1 4787 . 2 ((norm‘(𝐹𝐴)) = 0 → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ 0 ≤ ((normop𝑇) · (norm𝐴))))
2 cnlnadjlem.1 . . . . . . . . . 10 𝑇 ∈ LinOp
3 cnlnadjlem.2 . . . . . . . . . 10 𝑇 ∈ ContOp
4 cnlnadjlem.3 . . . . . . . . . 10 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
5 cnlnadjlem.4 . . . . . . . . . 10 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
6 cnlnadjlem.5 . . . . . . . . . 10 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
72, 3, 4, 5, 6cnlnadjlem4 29263 . . . . . . . . 9 (𝐴 ∈ ℋ → (𝐹𝐴) ∈ ℋ)
82lnopfi 29162 . . . . . . . . . 10 𝑇: ℋ⟶ ℋ
98ffvelrni 6501 . . . . . . . . 9 ((𝐹𝐴) ∈ ℋ → (𝑇‘(𝐹𝐴)) ∈ ℋ)
107, 9syl 17 . . . . . . . 8 (𝐴 ∈ ℋ → (𝑇‘(𝐹𝐴)) ∈ ℋ)
11 hicl 28271 . . . . . . . 8 (((𝑇‘(𝐹𝐴)) ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) ∈ ℂ)
1210, 11mpancom 660 . . . . . . 7 (𝐴 ∈ ℋ → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) ∈ ℂ)
1312abscld 14382 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ∈ ℝ)
14 normcl 28316 . . . . . . . 8 ((𝑇‘(𝐹𝐴)) ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ∈ ℝ)
1510, 14syl 17 . . . . . . 7 (𝐴 ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ∈ ℝ)
16 normcl 28316 . . . . . . 7 (𝐴 ∈ ℋ → (norm𝐴) ∈ ℝ)
1715, 16remulcld 10271 . . . . . 6 (𝐴 ∈ ℋ → ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)) ∈ ℝ)
182, 3nmcopexi 29220 . . . . . . . 8 (normop𝑇) ∈ ℝ
19 normcl 28316 . . . . . . . . 9 ((𝐹𝐴) ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℝ)
207, 19syl 17 . . . . . . . 8 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℝ)
21 remulcl 10222 . . . . . . . 8 (((normop𝑇) ∈ ℝ ∧ (norm‘(𝐹𝐴)) ∈ ℝ) → ((normop𝑇) · (norm‘(𝐹𝐴))) ∈ ℝ)
2218, 20, 21sylancr 567 . . . . . . 7 (𝐴 ∈ ℋ → ((normop𝑇) · (norm‘(𝐹𝐴))) ∈ ℝ)
2322, 16remulcld 10271 . . . . . 6 (𝐴 ∈ ℋ → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) ∈ ℝ)
24 bcs 28372 . . . . . . 7 (((𝑇‘(𝐹𝐴)) ∈ ℋ ∧ 𝐴 ∈ ℋ) → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)))
2510, 24mpancom 660 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)))
26 normge0 28317 . . . . . . 7 (𝐴 ∈ ℋ → 0 ≤ (norm𝐴))
272, 3nmcoplbi 29221 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ≤ ((normop𝑇) · (norm‘(𝐹𝐴))))
287, 27syl 17 . . . . . . 7 (𝐴 ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ≤ ((normop𝑇) · (norm‘(𝐹𝐴))))
2915, 22, 16, 26, 28lemul1ad 11164 . . . . . 6 (𝐴 ∈ ℋ → ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)) ≤ (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)))
3013, 17, 23, 25, 29letrd 10395 . . . . 5 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)))
312, 3, 4, 5, 6cnlnadjlem5 29264 . . . . . . . 8 ((𝐴 ∈ ℋ ∧ (𝐹𝐴) ∈ ℋ) → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) = ((𝐹𝐴) ·ih (𝐹𝐴)))
327, 31mpdan 659 . . . . . . 7 (𝐴 ∈ ℋ → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) = ((𝐹𝐴) ·ih (𝐹𝐴)))
3332fveq2d 6336 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) = (abs‘((𝐹𝐴) ·ih (𝐹𝐴))))
34 hiidrcl 28286 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) ∈ ℝ)
357, 34syl 17 . . . . . . 7 (𝐴 ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) ∈ ℝ)
36 hiidge0 28289 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → 0 ≤ ((𝐹𝐴) ·ih (𝐹𝐴)))
377, 36syl 17 . . . . . . 7 (𝐴 ∈ ℋ → 0 ≤ ((𝐹𝐴) ·ih (𝐹𝐴)))
3835, 37absidd 14368 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝐹𝐴) ·ih (𝐹𝐴))) = ((𝐹𝐴) ·ih (𝐹𝐴)))
39 normsq 28325 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((𝐹𝐴) ·ih (𝐹𝐴)))
407, 39syl 17 . . . . . . 7 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((𝐹𝐴) ·ih (𝐹𝐴)))
4120recnd 10269 . . . . . . . 8 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℂ)
4241sqvald 13211 . . . . . . 7 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4340, 42eqtr3d 2806 . . . . . 6 (𝐴 ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4433, 38, 433eqtrd 2808 . . . . 5 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4516recnd 10269 . . . . . 6 (𝐴 ∈ ℋ → (norm𝐴) ∈ ℂ)
4618recni 10253 . . . . . . 7 (normop𝑇) ∈ ℂ
47 mul32 10404 . . . . . . 7 (((normop𝑇) ∈ ℂ ∧ (norm‘(𝐹𝐴)) ∈ ℂ ∧ (norm𝐴) ∈ ℂ) → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
4846, 47mp3an1 1558 . . . . . 6 (((norm‘(𝐹𝐴)) ∈ ℂ ∧ (norm𝐴) ∈ ℂ) → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
4941, 45, 48syl2anc 565 . . . . 5 (𝐴 ∈ ℋ → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5030, 44, 493brtr3d 4815 . . . 4 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5150adantr 466 . . 3 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5220adantr 466 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → (norm‘(𝐹𝐴)) ∈ ℝ)
53 remulcl 10222 . . . . . 6 (((normop𝑇) ∈ ℝ ∧ (norm𝐴) ∈ ℝ) → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
5418, 16, 53sylancr 567 . . . . 5 (𝐴 ∈ ℋ → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
5554adantr 466 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
56 normge0 28317 . . . . . . 7 ((𝐹𝐴) ∈ ℋ → 0 ≤ (norm‘(𝐹𝐴)))
57 0re 10241 . . . . . . . 8 0 ∈ ℝ
58 leltne 10328 . . . . . . . 8 ((0 ∈ ℝ ∧ (norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 ≤ (norm‘(𝐹𝐴))) → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
5957, 58mp3an1 1558 . . . . . . 7 (((norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 ≤ (norm‘(𝐹𝐴))) → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
6019, 56, 59syl2anc 565 . . . . . 6 ((𝐹𝐴) ∈ ℋ → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
6160biimpar 463 . . . . 5 (((𝐹𝐴) ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → 0 < (norm‘(𝐹𝐴)))
627, 61sylan 561 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → 0 < (norm‘(𝐹𝐴)))
63 lemul1 11076 . . . 4 (((norm‘(𝐹𝐴)) ∈ ℝ ∧ ((normop𝑇) · (norm𝐴)) ∈ ℝ ∧ ((norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 < (norm‘(𝐹𝐴)))) → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴)))))
6452, 55, 52, 62, 63syl112anc 1479 . . 3 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴)))))
6551, 64mpbird 247 . 2 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))
66 nmopge0 29104 . . . . 5 (𝑇: ℋ⟶ ℋ → 0 ≤ (normop𝑇))
678, 66ax-mp 5 . . . 4 0 ≤ (normop𝑇)
68 mulge0 10747 . . . 4 ((((normop𝑇) ∈ ℝ ∧ 0 ≤ (normop𝑇)) ∧ ((norm𝐴) ∈ ℝ ∧ 0 ≤ (norm𝐴))) → 0 ≤ ((normop𝑇) · (norm𝐴)))
6918, 67, 68mpanl12 674 . . 3 (((norm𝐴) ∈ ℝ ∧ 0 ≤ (norm𝐴)) → 0 ≤ ((normop𝑇) · (norm𝐴)))
7016, 26, 69syl2anc 565 . 2 (𝐴 ∈ ℋ → 0 ≤ ((normop𝑇) · (norm𝐴)))
711, 65, 70pm2.61ne 3027 1 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))