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

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

Proof of Theorem cnlnadjlem7
StepHypRef Expression
1 breq1 4586 . 2 ((norm‘(𝐹𝐴)) = 0 → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ 0 ≤ ((normop𝑇) · (norm𝐴))))
2 cnlnadjlem.1 . . . . . . . . . 10 𝑇 ∈ LinOp
3 cnlnadjlem.2 . . . . . . . . . 10 𝑇 ∈ ConOp
4 cnlnadjlem.3 . . . . . . . . . 10 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
5 cnlnadjlem.4 . . . . . . . . . 10 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
6 cnlnadjlem.5 . . . . . . . . . 10 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
72, 3, 4, 5, 6cnlnadjlem4 28313 . . . . . . . . 9 (𝐴 ∈ ℋ → (𝐹𝐴) ∈ ℋ)
82lnopfi 28212 . . . . . . . . . 10 𝑇: ℋ⟶ ℋ
98ffvelrni 6266 . . . . . . . . 9 ((𝐹𝐴) ∈ ℋ → (𝑇‘(𝐹𝐴)) ∈ ℋ)
107, 9syl 17 . . . . . . . 8 (𝐴 ∈ ℋ → (𝑇‘(𝐹𝐴)) ∈ ℋ)
11 hicl 27321 . . . . . . . 8 (((𝑇‘(𝐹𝐴)) ∈ ℋ ∧ 𝐴 ∈ ℋ) → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) ∈ ℂ)
1210, 11mpancom 700 . . . . . . 7 (𝐴 ∈ ℋ → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) ∈ ℂ)
1312abscld 14023 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ∈ ℝ)
14 normcl 27366 . . . . . . . 8 ((𝑇‘(𝐹𝐴)) ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ∈ ℝ)
1510, 14syl 17 . . . . . . 7 (𝐴 ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ∈ ℝ)
16 normcl 27366 . . . . . . 7 (𝐴 ∈ ℋ → (norm𝐴) ∈ ℝ)
1715, 16remulcld 9949 . . . . . 6 (𝐴 ∈ ℋ → ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)) ∈ ℝ)
182, 3nmcopexi 28270 . . . . . . . 8 (normop𝑇) ∈ ℝ
19 normcl 27366 . . . . . . . . 9 ((𝐹𝐴) ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℝ)
207, 19syl 17 . . . . . . . 8 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℝ)
21 remulcl 9900 . . . . . . . 8 (((normop𝑇) ∈ ℝ ∧ (norm‘(𝐹𝐴)) ∈ ℝ) → ((normop𝑇) · (norm‘(𝐹𝐴))) ∈ ℝ)
2218, 20, 21sylancr 694 . . . . . . 7 (𝐴 ∈ ℋ → ((normop𝑇) · (norm‘(𝐹𝐴))) ∈ ℝ)
2322, 16remulcld 9949 . . . . . 6 (𝐴 ∈ ℋ → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) ∈ ℝ)
24 bcs 27422 . . . . . . 7 (((𝑇‘(𝐹𝐴)) ∈ ℋ ∧ 𝐴 ∈ ℋ) → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)))
2510, 24mpancom 700 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)))
26 normge0 27367 . . . . . . 7 (𝐴 ∈ ℋ → 0 ≤ (norm𝐴))
272, 3nmcoplbi 28271 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ≤ ((normop𝑇) · (norm‘(𝐹𝐴))))
287, 27syl 17 . . . . . . 7 (𝐴 ∈ ℋ → (norm‘(𝑇‘(𝐹𝐴))) ≤ ((normop𝑇) · (norm‘(𝐹𝐴))))
2915, 22, 16, 26, 28lemul1ad 10842 . . . . . 6 (𝐴 ∈ ℋ → ((norm‘(𝑇‘(𝐹𝐴))) · (norm𝐴)) ≤ (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)))
3013, 17, 23, 25, 29letrd 10073 . . . . 5 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) ≤ (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)))
312, 3, 4, 5, 6cnlnadjlem5 28314 . . . . . . . 8 ((𝐴 ∈ ℋ ∧ (𝐹𝐴) ∈ ℋ) → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) = ((𝐹𝐴) ·ih (𝐹𝐴)))
327, 31mpdan 699 . . . . . . 7 (𝐴 ∈ ℋ → ((𝑇‘(𝐹𝐴)) ·ih 𝐴) = ((𝐹𝐴) ·ih (𝐹𝐴)))
3332fveq2d 6107 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) = (abs‘((𝐹𝐴) ·ih (𝐹𝐴))))
34 hiidrcl 27336 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) ∈ ℝ)
357, 34syl 17 . . . . . . 7 (𝐴 ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) ∈ ℝ)
36 hiidge0 27339 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → 0 ≤ ((𝐹𝐴) ·ih (𝐹𝐴)))
377, 36syl 17 . . . . . . 7 (𝐴 ∈ ℋ → 0 ≤ ((𝐹𝐴) ·ih (𝐹𝐴)))
3835, 37absidd 14009 . . . . . 6 (𝐴 ∈ ℋ → (abs‘((𝐹𝐴) ·ih (𝐹𝐴))) = ((𝐹𝐴) ·ih (𝐹𝐴)))
39 normsq 27375 . . . . . . . 8 ((𝐹𝐴) ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((𝐹𝐴) ·ih (𝐹𝐴)))
407, 39syl 17 . . . . . . 7 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((𝐹𝐴) ·ih (𝐹𝐴)))
4120recnd 9947 . . . . . . . 8 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ∈ ℂ)
4241sqvald 12867 . . . . . . 7 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴))↑2) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4340, 42eqtr3d 2646 . . . . . 6 (𝐴 ∈ ℋ → ((𝐹𝐴) ·ih (𝐹𝐴)) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4433, 38, 433eqtrd 2648 . . . . 5 (𝐴 ∈ ℋ → (abs‘((𝑇‘(𝐹𝐴)) ·ih 𝐴)) = ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))))
4516recnd 9947 . . . . . 6 (𝐴 ∈ ℋ → (norm𝐴) ∈ ℂ)
4618recni 9931 . . . . . . 7 (normop𝑇) ∈ ℂ
47 mul32 10082 . . . . . . 7 (((normop𝑇) ∈ ℂ ∧ (norm‘(𝐹𝐴)) ∈ ℂ ∧ (norm𝐴) ∈ ℂ) → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
4846, 47mp3an1 1403 . . . . . 6 (((norm‘(𝐹𝐴)) ∈ ℂ ∧ (norm𝐴) ∈ ℂ) → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
4941, 45, 48syl2anc 691 . . . . 5 (𝐴 ∈ ℋ → (((normop𝑇) · (norm‘(𝐹𝐴))) · (norm𝐴)) = (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5030, 44, 493brtr3d 4614 . . . 4 (𝐴 ∈ ℋ → ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5150adantr 480 . . 3 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴))))
5220adantr 480 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → (norm‘(𝐹𝐴)) ∈ ℝ)
53 remulcl 9900 . . . . . 6 (((normop𝑇) ∈ ℝ ∧ (norm𝐴) ∈ ℝ) → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
5418, 16, 53sylancr 694 . . . . 5 (𝐴 ∈ ℋ → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
5554adantr 480 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((normop𝑇) · (norm𝐴)) ∈ ℝ)
56 normge0 27367 . . . . . . 7 ((𝐹𝐴) ∈ ℋ → 0 ≤ (norm‘(𝐹𝐴)))
57 0re 9919 . . . . . . . 8 0 ∈ ℝ
58 leltne 10006 . . . . . . . 8 ((0 ∈ ℝ ∧ (norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 ≤ (norm‘(𝐹𝐴))) → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
5957, 58mp3an1 1403 . . . . . . 7 (((norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 ≤ (norm‘(𝐹𝐴))) → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
6019, 56, 59syl2anc 691 . . . . . 6 ((𝐹𝐴) ∈ ℋ → (0 < (norm‘(𝐹𝐴)) ↔ (norm‘(𝐹𝐴)) ≠ 0))
6160biimpar 501 . . . . 5 (((𝐹𝐴) ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → 0 < (norm‘(𝐹𝐴)))
627, 61sylan 487 . . . 4 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → 0 < (norm‘(𝐹𝐴)))
63 lemul1 10754 . . . 4 (((norm‘(𝐹𝐴)) ∈ ℝ ∧ ((normop𝑇) · (norm𝐴)) ∈ ℝ ∧ ((norm‘(𝐹𝐴)) ∈ ℝ ∧ 0 < (norm‘(𝐹𝐴)))) → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴)))))
6452, 55, 52, 62, 63syl112anc 1322 . . 3 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → ((norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)) ↔ ((norm‘(𝐹𝐴)) · (norm‘(𝐹𝐴))) ≤ (((normop𝑇) · (norm𝐴)) · (norm‘(𝐹𝐴)))))
6551, 64mpbird 246 . 2 ((𝐴 ∈ ℋ ∧ (norm‘(𝐹𝐴)) ≠ 0) → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))
66 nmopge0 28154 . . . . 5 (𝑇: ℋ⟶ ℋ → 0 ≤ (normop𝑇))
678, 66ax-mp 5 . . . 4 0 ≤ (normop𝑇)
68 mulge0 10425 . . . 4 ((((normop𝑇) ∈ ℝ ∧ 0 ≤ (normop𝑇)) ∧ ((norm𝐴) ∈ ℝ ∧ 0 ≤ (norm𝐴))) → 0 ≤ ((normop𝑇) · (norm𝐴)))
6918, 67, 68mpanl12 714 . . 3 (((norm𝐴) ∈ ℝ ∧ 0 ≤ (norm𝐴)) → 0 ≤ ((normop𝑇) · (norm𝐴)))
7016, 26, 69syl2anc 691 . 2 (𝐴 ∈ ℋ → 0 ≤ ((normop𝑇) · (norm𝐴)))
711, 65, 70pm2.61ne 2867 1 (𝐴 ∈ ℋ → (norm‘(𝐹𝐴)) ≤ ((normop𝑇) · (norm𝐴)))