# 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 ∈ BndLinOp$
nmoptri.2 $⊢ T ∈ BndLinOp$
Assertion nmopcoi $⊢ norm op ⁡ S ∘ T ≤ norm op ⁡ S ⁢ norm op ⁡ T$

### Proof

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