# Metamath Proof Explorer

## Theorem nmophmi

Description: The norm of the scalar product of a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmophm.1 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion nmophmi ${⊢}{A}\in ℂ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)=\left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmophm.1 ${⊢}{T}\in \mathrm{BndLinOp}$
2 bdopf ${⊢}{T}\in \mathrm{BndLinOp}\to {T}:ℋ⟶ℋ$
3 1 2 ax-mp ${⊢}{T}:ℋ⟶ℋ$
4 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
5 3 4 mp3an2 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
6 5 fveq2d ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)={norm}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$
7 3 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
8 norm-iii ${⊢}\left({A}\in ℂ\wedge {T}\left({x}\right)\in ℋ\right)\to {norm}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right)=\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)$
9 7 8 sylan2 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right)=\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)$
10 6 9 eqtrd ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)=\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)$
11 10 adantr ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)=\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)$
12 normcl ${⊢}{T}\left({x}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
13 7 12 syl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
14 13 ad2antlr ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
15 abscl ${⊢}{A}\in ℂ\to \left|{A}\right|\in ℝ$
16 absge0 ${⊢}{A}\in ℂ\to 0\le \left|{A}\right|$
17 15 16 jca ${⊢}{A}\in ℂ\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
18 17 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
19 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)$
20 3 19 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)$
21 20 adantll ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
22 nmopre ${⊢}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
23 1 22 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
24 lemul2a ${⊢}\left(\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to \left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$
25 23 24 mp3anl2 ${⊢}\left(\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to \left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$
26 14 18 21 25 syl21anc ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$
27 11 26 eqbrtrd ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$
28 27 ex ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\right)$
29 28 ralrimiva ${⊢}{A}\in ℂ\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\right)$
30 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
31 3 30 mpan2 ${⊢}{A}\in ℂ\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
32 remulcl ${⊢}\left(\left|{A}\right|\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right)\in ℝ\right)\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
33 15 23 32 sylancl ${⊢}{A}\in ℂ\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
34 33 rexrd ${⊢}{A}\in ℂ\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}$
35 nmopub ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\le \left|{A}\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({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\right)\right)$
36 31 34 35 syl2anc ${⊢}{A}\in ℂ\to \left({norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\le \left|{A}\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({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\right)\right)$
37 29 36 mpbird ${⊢}{A}\in ℂ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$
38 fveq2 ${⊢}{A}=0\to \left|{A}\right|=\left|0\right|$
39 abs0 ${⊢}\left|0\right|=0$
40 38 39 syl6eq ${⊢}{A}=0\to \left|{A}\right|=0$
41 40 oveq1d ${⊢}{A}=0\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)=0\cdot {norm}_{\mathrm{op}}\left({T}\right)$
42 23 recni ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℂ$
43 42 mul02i ${⊢}0\cdot {norm}_{\mathrm{op}}\left({T}\right)=0$
44 41 43 syl6eq ${⊢}{A}=0\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)=0$
45 44 adantl ${⊢}\left({A}\in ℂ\wedge {A}=0\right)\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)=0$
46 nmopge0 ${⊢}\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to 0\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
47 31 46 syl ${⊢}{A}\in ℂ\to 0\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
48 47 adantr ${⊢}\left({A}\in ℂ\wedge {A}=0\right)\to 0\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
49 45 48 eqbrtrd ${⊢}\left({A}\in ℂ\wedge {A}=0\right)\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
50 nmoplb ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
51 31 50 syl3an1 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
52 51 3expa ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
53 11 52 eqbrtrrd ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
54 53 adantllr ${⊢}\left(\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
55 13 adantl ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
56 nmopxr ${⊢}\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}$
57 31 56 syl ${⊢}{A}\in ℂ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}$
58 nmopgtmnf ${⊢}\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
59 31 58 syl ${⊢}{A}\in ℂ\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
60 xrre ${⊢}\left(\left({norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}\wedge \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }<{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\wedge {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\right)\right)\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ$
61 57 33 59 37 60 syl22anc ${⊢}{A}\in ℂ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ$
62 61 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ$
63 15 ad2antrr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to \left|{A}\right|\in ℝ$
64 absgt0 ${⊢}{A}\in ℂ\to \left({A}\ne 0↔0<\left|{A}\right|\right)$
65 64 biimpa ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to 0<\left|{A}\right|$
66 65 adantr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to 0<\left|{A}\right|$
67 lemuldiv2 ${⊢}\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0<\left|{A}\right|\right)\right)\to \left(\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)↔{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
68 55 62 63 66 67 syl112anc ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to \left(\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)↔{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
69 68 adantr ${⊢}\left(\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left(\left|{A}\right|{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)↔{norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
70 54 69 mpbid ${⊢}\left(\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}$
71 70 ex ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℋ\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
72 71 ralrimiva ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
73 61 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ$
74 15 adantr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\in ℝ$
75 abs00 ${⊢}{A}\in ℂ\to \left(\left|{A}\right|=0↔{A}=0\right)$
76 75 necon3bid ${⊢}{A}\in ℂ\to \left(\left|{A}\right|\ne 0↔{A}\ne 0\right)$
77 76 biimpar ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|\ne 0$
78 73 74 77 redivcld ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\in ℝ$
79 78 rexrd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\in {ℝ}^{*}$
80 nmopub ${⊢}\left({T}:ℋ⟶ℋ\wedge \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)\right)$
81 3 79 80 sylancr ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)\right)$
82 72 81 mpbird ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {norm}_{\mathrm{op}}\left({T}\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}$
83 23 a1i ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
84 lemuldiv2 ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0<\left|{A}\right|\right)\right)\to \left(\left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)↔{norm}_{\mathrm{op}}\left({T}\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
85 83 73 74 65 84 syl112anc ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)↔{norm}_{\mathrm{op}}\left({T}\right)\le \frac{{norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)}{\left|{A}\right|}\right)$
86 82 85 mpbird ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
87 49 86 pm2.61dane ${⊢}{A}\in ℂ\to \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
88 61 33 letri3d ${⊢}{A}\in ℂ\to \left({norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)=\left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)↔\left({norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\le \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\wedge \left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\right)$
89 37 87 88 mpbir2and ${⊢}{A}\in ℂ\to {norm}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)=\left|{A}\right|{norm}_{\mathrm{op}}\left({T}\right)$