Metamath Proof Explorer

Theorem bdophdi

Description: The difference between two bounded linear operators is bounded. (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 bdophdi ${⊢}{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 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 honegsubi ${⊢}{S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)={S}{-}_{\mathrm{op}}{T}$
8 neg1cn ${⊢}-1\in ℂ$
9 2 bdophmi ${⊢}-1\in ℂ\to -1{·}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$
10 8 9 ax-mp ${⊢}-1{·}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$
11 1 10 bdophsi ${⊢}{S}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{T}\right)\in \mathrm{BndLinOp}$
12 7 11 eqeltrri ${⊢}{S}{-}_{\mathrm{op}}{T}\in \mathrm{BndLinOp}$