Metamath Proof Explorer

Theorem nmopadjlem

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

Ref Expression
Hypothesis nmopadjle.1 ⊢ T ∈ BndLinOp
Assertion nmopadjlem ⊢ norm op ⁡ adj h ⁡ T ≤ norm op ⁡ T

Proof

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