Step |
Hyp |
Ref |
Expression |
1 |
|
nmopadjle.1 |
⊢ 𝑇 ∈ BndLinOp |
2 |
|
adjbdln |
⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp ) |
3 |
|
bdopf |
⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ) |
4 |
1 2 3
|
mp2b |
⊢ ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ |
5 |
|
bdopf |
⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ ) |
6 |
|
nmopxr |
⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* ) |
7 |
1 5 6
|
mp2b |
⊢ ( normop ‘ 𝑇 ) ∈ ℝ* |
8 |
|
nmopub |
⊢ ( ( ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ ∧ ( normop ‘ 𝑇 ) ∈ ℝ* ) → ( ( normop ‘ ( adjℎ ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑇 ) ↔ ∀ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( normop ‘ 𝑇 ) ) ) ) |
9 |
4 7 8
|
mp2an |
⊢ ( ( normop ‘ ( adjℎ ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑇 ) ↔ ∀ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( normop ‘ 𝑇 ) ) ) |
10 |
4
|
ffvelrni |
⊢ ( 𝑦 ∈ ℋ → ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ ) |
11 |
|
normcl |
⊢ ( ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℝ ) |
12 |
10 11
|
syl |
⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℝ ) |
13 |
12
|
adantr |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ∈ ℝ ) |
14 |
|
nmopre |
⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ ) |
15 |
1 14
|
ax-mp |
⊢ ( normop ‘ 𝑇 ) ∈ ℝ |
16 |
|
normcl |
⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ ) |
17 |
|
remulcl |
⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ) |
18 |
15 16 17
|
sylancr |
⊢ ( 𝑦 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ) |
19 |
18
|
adantr |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ) |
20 |
|
1re |
⊢ 1 ∈ ℝ |
21 |
15 20
|
remulcli |
⊢ ( ( normop ‘ 𝑇 ) · 1 ) ∈ ℝ |
22 |
21
|
a1i |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · 1 ) ∈ ℝ ) |
23 |
1
|
nmopadjlei |
⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) |
25 |
|
nmopge0 |
⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) ) |
26 |
1 5 25
|
mp2b |
⊢ 0 ≤ ( normop ‘ 𝑇 ) |
27 |
15 26
|
pm3.2i |
⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 ≤ ( normop ‘ 𝑇 ) ) |
28 |
|
lemul2a |
⊢ ( ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 ≤ ( normop ‘ 𝑇 ) ) ) ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · 1 ) ) |
29 |
27 28
|
mp3anl3 |
⊢ ( ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · 1 ) ) |
30 |
20 29
|
mpanl2 |
⊢ ( ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · 1 ) ) |
31 |
16 30
|
sylan |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · 1 ) ) |
32 |
13 19 22 24 31
|
letrd |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · 1 ) ) |
33 |
15
|
recni |
⊢ ( normop ‘ 𝑇 ) ∈ ℂ |
34 |
33
|
mulid1i |
⊢ ( ( normop ‘ 𝑇 ) · 1 ) = ( normop ‘ 𝑇 ) |
35 |
32 34
|
breqtrdi |
⊢ ( ( 𝑦 ∈ ℋ ∧ ( normℎ ‘ 𝑦 ) ≤ 1 ) → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( normop ‘ 𝑇 ) ) |
36 |
35
|
ex |
⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ≤ 1 → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝑦 ) ) ≤ ( normop ‘ 𝑇 ) ) ) |
37 |
9 36
|
mprgbir |
⊢ ( normop ‘ ( adjℎ ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑇 ) |