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 ⊢normop⁡adjh⁡T≤normop⁡T

Proof

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