# Metamath Proof Explorer

## 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 ffvelrni ( 𝑥 ∈ ℋ → ( ( 𝑆𝑇 ) ‘ 𝑥 ) ∈ ℋ )
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 ffvelrni ( 𝑥 ∈ ℋ → ( 𝑇𝑥 ) ∈ ℋ )
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 mulid2i ( 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𝑇 ) )