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

 Description: Lemma for nmopadji 29877. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
Hypothesis
Ref Expression
Assertion
Ref Expression

Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nmopadjle.1 . . . 4 𝑇 ∈ BndLinOp
2 adjbdln 29870 . . . 4 (𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)
3 bdopf 29649 . . . 4 ((adj𝑇) ∈ BndLinOp → (adj𝑇): ℋ⟶ ℋ)
41, 2, 3mp2b 10 . . 3 (adj𝑇): ℋ⟶ ℋ
5 bdopf 29649 . . . 4 (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
6 nmopxr 29653 . . . 4 (𝑇: ℋ⟶ ℋ → (normop𝑇) ∈ ℝ*)
71, 5, 6mp2b 10 . . 3 (normop𝑇) ∈ ℝ*
8 nmopub 29695 . . 3 (((adj𝑇): ℋ⟶ ℋ ∧ (normop𝑇) ∈ ℝ*) → ((normop‘(adj𝑇)) ≤ (normop𝑇) ↔ ∀𝑦 ∈ ℋ ((norm𝑦) ≤ 1 → (norm‘((adj𝑇)‘𝑦)) ≤ (normop𝑇))))
94, 7, 8mp2an 691 . 2 ((normop‘(adj𝑇)) ≤ (normop𝑇) ↔ ∀𝑦 ∈ ℋ ((norm𝑦) ≤ 1 → (norm‘((adj𝑇)‘𝑦)) ≤ (normop𝑇)))
104ffvelrni 6831 . . . . . . 7 (𝑦 ∈ ℋ → ((adj𝑇)‘𝑦) ∈ ℋ)
11 normcl 28912 . . . . . . 7 (((adj𝑇)‘𝑦) ∈ ℋ → (norm‘((adj𝑇)‘𝑦)) ∈ ℝ)
1210, 11syl 17 . . . . . 6 (𝑦 ∈ ℋ → (norm‘((adj𝑇)‘𝑦)) ∈ ℝ)
1312adantr 484 . . . . 5 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → (norm‘((adj𝑇)‘𝑦)) ∈ ℝ)
14 nmopre 29657 . . . . . . . 8 (𝑇 ∈ BndLinOp → (normop𝑇) ∈ ℝ)
151, 14ax-mp 5 . . . . . . 7 (normop𝑇) ∈ ℝ
16 normcl 28912 . . . . . . 7 (𝑦 ∈ ℋ → (norm𝑦) ∈ ℝ)
17 remulcl 10615 . . . . . . 7 (((normop𝑇) ∈ ℝ ∧ (norm𝑦) ∈ ℝ) → ((normop𝑇) · (norm𝑦)) ∈ ℝ)
1815, 16, 17sylancr 590 . . . . . 6 (𝑦 ∈ ℋ → ((normop𝑇) · (norm𝑦)) ∈ ℝ)
1918adantr 484 . . . . 5 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · (norm𝑦)) ∈ ℝ)
20 1re 10634 . . . . . . 7 1 ∈ ℝ
2115, 20remulcli 10650 . . . . . 6 ((normop𝑇) · 1) ∈ ℝ
2221a1i 11 . . . . 5 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · 1) ∈ ℝ)
231nmopadjlei 29875 . . . . . 6 (𝑦 ∈ ℋ → (norm‘((adj𝑇)‘𝑦)) ≤ ((normop𝑇) · (norm𝑦)))
2423adantr 484 . . . . 5 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → (norm‘((adj𝑇)‘𝑦)) ≤ ((normop𝑇) · (norm𝑦)))
25 nmopge0 29698 . . . . . . . . . 10 (𝑇: ℋ⟶ ℋ → 0 ≤ (normop𝑇))
261, 5, 25mp2b 10 . . . . . . . . 9 0 ≤ (normop𝑇)
2715, 26pm3.2i 474 . . . . . . . 8 ((normop𝑇) ∈ ℝ ∧ 0 ≤ (normop𝑇))
28 lemul2a 11488 . . . . . . . 8 ((((norm𝑦) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((normop𝑇) ∈ ℝ ∧ 0 ≤ (normop𝑇))) ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · (norm𝑦)) ≤ ((normop𝑇) · 1))
2927, 28mp3anl3 1454 . . . . . . 7 ((((norm𝑦) ∈ ℝ ∧ 1 ∈ ℝ) ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · (norm𝑦)) ≤ ((normop𝑇) · 1))
3020, 29mpanl2 700 . . . . . 6 (((norm𝑦) ∈ ℝ ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · (norm𝑦)) ≤ ((normop𝑇) · 1))
3116, 30sylan 583 . . . . 5 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → ((normop𝑇) · (norm𝑦)) ≤ ((normop𝑇) · 1))
3213, 19, 22, 24, 31letrd 10790 . . . 4 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → (norm‘((adj𝑇)‘𝑦)) ≤ ((normop𝑇) · 1))
3315recni 10648 . . . . 5 (normop𝑇) ∈ ℂ
3433mulid1i 10638 . . . 4 ((normop𝑇) · 1) = (normop𝑇)
3532, 34breqtrdi 5074 . . 3 ((𝑦 ∈ ℋ ∧ (norm𝑦) ≤ 1) → (norm‘((adj𝑇)‘𝑦)) ≤ (normop𝑇))
3635ex 416 . 2 (𝑦 ∈ ℋ → ((norm𝑦) ≤ 1 → (norm‘((adj𝑇)‘𝑦)) ≤ (normop𝑇)))
379, 36mprgbir 3124 1 (normop‘(adj𝑇)) ≤ (normop𝑇)