Metamath Proof Explorer


Theorem nmopadjlem

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

Ref Expression
Hypothesis nmopadjle.1 𝑇 ∈ BndLinOp
Assertion nmopadjlem ( normop ‘ ( adj𝑇 ) ) ≤ ( normop𝑇 )

Proof

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𝑇 )