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