# Metamath Proof Explorer

## Theorem nmoptrii

Description: Triangle inequality for the norms of 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 nmoptrii ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{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 bdopf ${⊢}{S}\in \mathrm{BndLinOp}\to {S}:ℋ⟶ℋ$
4 1 3 ax-mp ${⊢}{S}:ℋ⟶ℋ$
5 bdopf ${⊢}{T}\in \mathrm{BndLinOp}\to {T}:ℋ⟶ℋ$
6 2 5 ax-mp ${⊢}{T}:ℋ⟶ℋ$
7 4 6 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
8 nmopre ${⊢}{S}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
9 1 8 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
10 nmopre ${⊢}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
11 2 10 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
12 9 11 readdcli ${⊢}{norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
13 12 rexri ${⊢}{norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}$
14 nmopub ${⊢}\left(\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{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}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)\right)$
15 7 13 14 mp2an ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{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}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
16 4 6 hoscli ${⊢}{x}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\in ℋ$
17 normcl ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\in ℋ\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\in ℝ$
18 16 17 syl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\in ℝ$
19 18 adantr ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\in ℝ$
20 4 ffvelrni ${⊢}{x}\in ℋ\to {S}\left({x}\right)\in ℋ$
21 normcl ${⊢}{S}\left({x}\right)\in ℋ\to {norm}_{ℎ}\left({S}\left({x}\right)\right)\in ℝ$
22 20 21 syl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({S}\left({x}\right)\right)\in ℝ$
23 6 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
24 normcl ${⊢}{T}\left({x}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
25 23 24 syl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
26 22 25 readdcld ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
27 26 adantr ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
28 12 a1i ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
29 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
30 4 6 29 mp3an12 ${⊢}{x}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
31 30 fveq2d ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)={norm}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
32 norm-ii ${⊢}\left({S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to {norm}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)\le {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)$
33 20 23 32 syl2anc ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)\le {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)$
34 31 33 eqbrtrd ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)$
35 34 adantr ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)$
36 nmoplb ${⊢}\left({S}:ℋ⟶ℋ\wedge {x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)$
37 4 36 mp3an1 ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)$
38 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)$
39 6 38 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)$
40 le2add ${⊢}\left(\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\in ℝ\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\right)\wedge \left({norm}_{\mathrm{op}}\left({S}\right)\in ℝ\wedge {norm}_{\mathrm{op}}\left({T}\right)\in ℝ\right)\right)\to \left(\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
41 9 11 40 mpanr12 ${⊢}\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\in ℝ\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\right)\to \left(\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
42 22 25 41 syl2anc ${⊢}{x}\in ℋ\to \left(\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
43 42 adantr ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left(\left({norm}_{ℎ}\left({S}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)\wedge {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
44 37 39 43 mp2and ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({S}\left({x}\right)\right)+{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
45 19 27 28 35 44 letrd ${⊢}\left({x}\in ℋ\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
46 45 ex ${⊢}{x}\in ℋ\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left(\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)$
47 15 46 mprgbir ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)$