# 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 ${⊢}{S}\in \mathrm{BndLinOp}$
nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion nmopcoi ${⊢}{norm}_{\mathrm{op}}\left({S}\circ {T}\right)\le {norm}_{\mathrm{op}}\left({S}\right){norm}_{\mathrm{op}}\left({T}\right)$

### Proof

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