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