This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( ( 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 mulridi ⊢ ( ( 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 ‘ 𝑇 )