Theorem nmopcoi

Description: Upper bound for the norm of the composition of two bounded linear operators. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoptri.1	⊢ 𝑆 ∈ BndLinOp
	nmoptri.2	⊢ 𝑇 ∈ BndLinOp
Assertion	nmopcoi	⊢ ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	⊢ 𝑆 ∈ BndLinOp
2		nmoptri.2	⊢ 𝑇 ∈ BndLinOp
3		bdopln	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp )
4	1 3	ax-mp	⊢ 𝑆 ∈ LinOp
5		bdopln	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
6	2 5	ax-mp	⊢ 𝑇 ∈ LinOp
7	4 6	lnopcoi	⊢ ( 𝑆 ∘ 𝑇 ) ∈ LinOp
8	7	lnopfi	⊢ ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ
9		nmopre	⊢ ( 𝑆 ∈ BndLinOp → ( normop ‘ 𝑆 ) ∈ ℝ )
10	1 9	ax-mp	⊢ ( normop ‘ 𝑆 ) ∈ ℝ
11		nmopre	⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
12	2 11	ax-mp	⊢ ( normop ‘ 𝑇 ) ∈ ℝ
13	10 12	remulcli	⊢ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ
14	13	rexri	⊢ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ*
15		nmopub	⊢ ( ( ( 𝑆 ∘ 𝑇 ) : ℋ ⟶ ℋ ∧ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ∈ ℝ* ) → ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) ) )
16	8 14 15	mp2an	⊢ ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
17		0le0	⊢ 0 ≤ 0
18	17	a1i	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → 0 ≤ 0 )
19	4 6	lnopco0i	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 )
20	7	nmlnop0iHIL	⊢ ( ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) = 0 ↔ ( 𝑆 ∘ 𝑇 ) = 0hop )
21	19 20	sylib	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( 𝑆 ∘ 𝑇 ) = 0hop )
22		fveq1	⊢ ( ( 𝑆 ∘ 𝑇 ) = 0hop → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 0hop ‘ 𝑥 ) )
23	22	fveq2d	⊢ ( ( 𝑆 ∘ 𝑇 ) = 0hop → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) )
24		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
25	24	fveq2d	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) = ( normℎ ‘ 0ℎ ) )
26		norm0	⊢ ( normℎ ‘ 0ℎ ) = 0
27	25 26	eqtrdi	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 0hop ‘ 𝑥 ) ) = 0 )
28	23 27	sylan9eq	⊢ ( ( ( 𝑆 ∘ 𝑇 ) = 0hop ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = 0 )
29	21 28	sylan	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = 0 )
30		oveq2	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = ( ( normop ‘ 𝑆 ) · 0 ) )
31	10	recni	⊢ ( normop ‘ 𝑆 ) ∈ ℂ
32	31	mul01i	⊢ ( ( normop ‘ 𝑆 ) · 0 ) = 0
33	30 32	eqtrdi	⊢ ( ( normop ‘ 𝑇 ) = 0 → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = 0 )
34	33	adantr	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) = 0 )
35	18 29 34	3brtr4d	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
36	35	adantrr	⊢ ( ( ( normop ‘ 𝑇 ) = 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
37		df-ne	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ ¬ ( normop ‘ 𝑇 ) = 0 )
38	8	ffvelcdmi	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ )
39		normcl	⊢ ( ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
40	38 39	syl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
41	40	recnd	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ )
42	12	recni	⊢ ( normop ‘ 𝑇 ) ∈ ℂ
43		divrec2	⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
44	42 43	mp3an2	⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
45	41 44	sylan	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
46	45	ancoms	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
47	12	rerecclzi	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
48		bdopf	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
49	2 48	ax-mp	⊢ 𝑇 : ℋ ⟶ ℋ
50		nmopgt0	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) ) )
51	49 50	ax-mp	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 0 < ( normop ‘ 𝑇 ) )
52	12	recgt0i	⊢ ( 0 < ( normop ‘ 𝑇 ) → 0 < ( 1 / ( normop ‘ 𝑇 ) ) )
53	51 52	sylbi	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 < ( 1 / ( normop ‘ 𝑇 ) ) )
54		0re	⊢ 0 ∈ ℝ
55		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
56	54 55	mpan	⊢ ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ → ( 0 < ( 1 / ( normop ‘ 𝑇 ) ) → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) ) )
57	47 53 56	sylc	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 ≤ ( 1 / ( normop ‘ 𝑇 ) ) )
58	47 57	absidd	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) = ( 1 / ( normop ‘ 𝑇 ) ) )
59	58	adantr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) = ( 1 / ( normop ‘ 𝑇 ) ) )
60	59	oveq1d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
61	46 60	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
62	42	recclzi	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ )
63		norm-iii	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
64	62 38 63	syl2an	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
65	61 64	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
66	49	ffvelcdmi	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
67	4	lnopmuli	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
68	62 66 67	syl2an	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
69		bdopf	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
70	1 69	ax-mp	⊢ 𝑆 : ℋ ⟶ ℋ
71	70 49	hocoi	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) )
72	71	oveq2d	⊢ ( 𝑥 ∈ ℋ → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
73	72	adantl	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑆 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
74	68 73	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) )
75	74	fveq2d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) = ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ) )
76	65 75	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
77	76	adantrr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) )
78		hvmulcl	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
79	62 66 78	syl2an	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
80	79	adantrr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
81		norm-iii	⊢ ( ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
82	62 66 81	syl2an	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
83		normcl	⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
84	66 83	syl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
85	84	recnd	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ )
86		divrec2	⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
87	42 86	mp3an2	⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
88	85 87	sylan	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
89	88	ancoms	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
90	59	oveq1d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 1 / ( normop ‘ 𝑇 ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
91	89 90	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) = ( ( abs ‘ ( 1 / ( normop ‘ 𝑇 ) ) ) · ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
92	82 91	eqtr4d	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) )
93	92	adantrr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) )
94		nmoplb	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
95	49 94	mp3an1	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
96	42	mullidi	⊢ ( 1 · ( normop ‘ 𝑇 ) ) = ( normop ‘ 𝑇 )
97	95 96	breqtrrdi	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) )
98	97	adantl	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) )
99	84	adantr	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
100		1red	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 1 ∈ ℝ )
101	12	a1i	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( normop ‘ 𝑇 ) ∈ ℝ )
102	51	biimpi	⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → 0 < ( normop ‘ 𝑇 ) )
103	102	adantl	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → 0 < ( normop ‘ 𝑇 ) )
104		ledivmul2	⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
105	99 100 101 103 104	syl112anc	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normop ‘ 𝑇 ) ≠ 0 ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
106	105	ancoms	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ 𝑥 ∈ ℋ ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
107	106	adantrr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 · ( normop ‘ 𝑇 ) ) ) )
108	98 107	mpbird	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ 1 )
109	93 108	eqbrtrd	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 )
110		nmoplb	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
111	70 110	mp3an1	⊢ ( ( ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
112	80 109 111	syl2anc	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( 𝑆 ‘ ( ( 1 / ( normop ‘ 𝑇 ) ) ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) ≤ ( normop ‘ 𝑆 ) )
113	77 112	eqbrtrd	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) )
114	40	ad2antrl	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
115	10	a1i	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normop ‘ 𝑆 ) ∈ ℝ )
116	102	adantr	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → 0 < ( normop ‘ 𝑇 ) )
117	116 12	jctil	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) )
118		ledivmul2	⊢ ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ( normop ‘ 𝑆 ) ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( normop ‘ 𝑇 ) ) ) → ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) ↔ ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
119	114 115 117 118	syl3anc	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) / ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ 𝑆 ) ↔ ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
120	113 119	mpbid	⊢ ( ( ( normop ‘ 𝑇 ) ≠ 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
121	37 120	sylanbr	⊢ ( ( ¬ ( normop ‘ 𝑇 ) = 0 ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
122	36 121	pm2.61ian	⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) )
123	122	ex	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 ∘ 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) ) ) )
124	16 123	mprgbir	⊢ ( normop ‘ ( 𝑆 ∘ 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) · ( normop ‘ 𝑇 ) )