# Metamath Proof Explorer

## Theorem nmoptri2i

Description: Triangle-type 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 nmoptri2i ${⊢}{norm}_{\mathrm{op}}\left({S}\right)-{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$

### Proof

Step Hyp Ref Expression
1 nmoptri.1 ${⊢}{S}\in \mathrm{BndLinOp}$
2 nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
3 1 2 bdophsi ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$
4 neg1cn ${⊢}-1\in ℂ$
5 2 bdophmi ${⊢}-1\in ℂ\to -1{·}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$
6 4 5 ax-mp ${⊢}-1{·}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$
7 3 6 nmoptrii ${⊢}{norm}_{\mathrm{op}}\left(\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)+{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)$
8 bdopf ${⊢}{S}\in \mathrm{BndLinOp}\to {S}:ℋ⟶ℋ$
9 1 8 ax-mp ${⊢}{S}:ℋ⟶ℋ$
10 bdopf ${⊢}{T}\in \mathrm{BndLinOp}\to {T}:ℋ⟶ℋ$
11 2 10 ax-mp ${⊢}{T}:ℋ⟶ℋ$
12 9 11 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
13 12 11 honegsubi ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)=\left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{T}$
14 9 11 hopncani ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{T}={S}$
15 13 14 eqtri ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={S}$
16 15 fveq2i ${⊢}{norm}_{\mathrm{op}}\left(\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)\right)={norm}_{\mathrm{op}}\left({S}\right)$
17 11 nmopnegi ${⊢}{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={norm}_{\mathrm{op}}\left({T}\right)$
18 17 oveq2i ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)+{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
19 7 16 18 3brtr3i ${⊢}{norm}_{\mathrm{op}}\left({S}\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
20 nmopre ${⊢}{S}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
21 1 20 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
22 nmopre ${⊢}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
23 2 22 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
24 nmopre ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in ℝ$
25 3 24 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in ℝ$
26 21 23 25 lesubaddi ${⊢}{norm}_{\mathrm{op}}\left({S}\right)-{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)↔{norm}_{\mathrm{op}}\left({S}\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
27 19 26 mpbir ${⊢}{norm}_{\mathrm{op}}\left({S}\right)-{norm}_{\mathrm{op}}\left({T}\right)\le {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$