# Metamath Proof Explorer

## Theorem bdophsi

Description: The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1 ${⊢}{S}\in \mathrm{BndLinOp}$
nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion bdophsi ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$

### Proof

Step Hyp Ref Expression
1 nmoptri.1 ${⊢}{S}\in \mathrm{BndLinOp}$
2 nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
3 bdopln ${⊢}{S}\in \mathrm{BndLinOp}\to {S}\in \mathrm{LinOp}$
4 1 3 ax-mp ${⊢}{S}\in \mathrm{LinOp}$
5 bdopln ${⊢}{T}\in \mathrm{BndLinOp}\to {T}\in \mathrm{LinOp}$
6 2 5 ax-mp ${⊢}{T}\in \mathrm{LinOp}$
7 4 6 lnophsi ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{LinOp}$
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 nmopxr ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}$
14 12 13 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}$
15 nmopre ${⊢}{S}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
16 1 15 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({S}\right)\in ℝ$
17 nmopre ${⊢}{T}\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
18 2 17 ax-mp ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
19 16 18 readdcli ${⊢}{norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
20 nmopgtmnf ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$
21 12 20 ax-mp ${⊢}\mathrm{-\infty }<{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$
22 1 2 nmoptrii ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)$
23 xrre ${⊢}\left(\left({norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }<{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\wedge {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\le {norm}_{\mathrm{op}}\left({S}\right)+{norm}_{\mathrm{op}}\left({T}\right)\right)\right)\to {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in ℝ$
24 14 19 21 22 23 mp4an ${⊢}{norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in ℝ$
25 elbdop2 ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}↔\left({S}{+}_{\mathrm{op}}{T}\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\in ℝ\right)$
26 7 24 25 mpbir2an ${⊢}{S}{+}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$