# 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 e. BndLinOp`
nmoptri.2
`|- T e. BndLinOp`
Assertion nmoptri2i
`|- ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) )`

### Proof

Step Hyp Ref Expression
1 nmoptri.1
` |-  S e. BndLinOp`
2 nmoptri.2
` |-  T e. BndLinOp`
3 1 2 bdophsi
` |-  ( S +op T ) e. BndLinOp`
4 neg1cn
` |-  -u 1 e. CC`
5 2 bdophmi
` |-  ( -u 1 e. CC -> ( -u 1 .op T ) e. BndLinOp )`
6 4 5 ax-mp
` |-  ( -u 1 .op T ) e. BndLinOp`
7 3 6 nmoptrii
` |-  ( normop ` ( ( S +op T ) +op ( -u 1 .op T ) ) ) <_ ( ( normop ` ( S +op T ) ) + ( normop ` ( -u 1 .op T ) ) )`
8 bdopf
` |-  ( S e. BndLinOp -> S : ~H --> ~H )`
9 1 8 ax-mp
` |-  S : ~H --> ~H`
10 bdopf
` |-  ( T e. BndLinOp -> T : ~H --> ~H )`
11 2 10 ax-mp
` |-  T : ~H --> ~H`
` |-  ( S +op T ) : ~H --> ~H`
13 12 11 honegsubi
` |-  ( ( S +op T ) +op ( -u 1 .op T ) ) = ( ( S +op T ) -op T )`
14 9 11 hopncani
` |-  ( ( S +op T ) -op T ) = S`
15 13 14 eqtri
` |-  ( ( S +op T ) +op ( -u 1 .op T ) ) = S`
16 15 fveq2i
` |-  ( normop ` ( ( S +op T ) +op ( -u 1 .op T ) ) ) = ( normop ` S )`
17 11 nmopnegi
` |-  ( normop ` ( -u 1 .op T ) ) = ( normop ` T )`
18 17 oveq2i
` |-  ( ( normop ` ( S +op T ) ) + ( normop ` ( -u 1 .op T ) ) ) = ( ( normop ` ( S +op T ) ) + ( normop ` T ) )`
19 7 16 18 3brtr3i
` |-  ( normop ` S ) <_ ( ( normop ` ( S +op T ) ) + ( normop ` T ) )`
20 nmopre
` |-  ( S e. BndLinOp -> ( normop ` S ) e. RR )`
21 1 20 ax-mp
` |-  ( normop ` S ) e. RR`
22 nmopre
` |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )`
23 2 22 ax-mp
` |-  ( normop ` T ) e. RR`
24 nmopre
` |-  ( ( S +op T ) e. BndLinOp -> ( normop ` ( S +op T ) ) e. RR )`
25 3 24 ax-mp
` |-  ( normop ` ( S +op T ) ) e. RR`
` |-  ( ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) ) <-> ( normop ` S ) <_ ( ( normop ` ( S +op T ) ) + ( normop ` T ) ) )`
` |-  ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) )`