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

### Proof

Step Hyp Ref Expression
1 nmoptri.1
` |-  S e. BndLinOp`
2 nmoptri.2
` |-  T e. BndLinOp`
3 bdopf
` |-  ( S e. BndLinOp -> S : ~H --> ~H )`
4 1 3 ax-mp
` |-  S : ~H --> ~H`
5 bdopf
` |-  ( T e. BndLinOp -> T : ~H --> ~H )`
6 2 5 ax-mp
` |-  T : ~H --> ~H`
` |-  ( S +op T ) : ~H --> ~H`
8 nmopre
` |-  ( S e. BndLinOp -> ( normop ` S ) e. RR )`
9 1 8 ax-mp
` |-  ( normop ` S ) e. RR`
10 nmopre
` |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )`
11 2 10 ax-mp
` |-  ( normop ` T ) e. RR`
` |-  ( ( normop ` S ) + ( normop ` T ) ) e. RR`
13 12 rexri
` |-  ( ( normop ` S ) + ( normop ` T ) ) e. RR*`
14 nmopub
` |-  ( ( ( S +op T ) : ~H --> ~H /\ ( ( normop ` S ) + ( normop ` T ) ) e. RR* ) -> ( ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) ) )`
15 7 13 14 mp2an
` |-  ( ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
16 4 6 hoscli
` |-  ( x e. ~H -> ( ( S +op T ) ` x ) e. ~H )`
17 normcl
` |-  ( ( ( S +op T ) ` x ) e. ~H -> ( normh ` ( ( S +op T ) ` x ) ) e. RR )`
18 16 17 syl
` |-  ( x e. ~H -> ( normh ` ( ( S +op T ) ` x ) ) e. RR )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( S +op T ) ` x ) ) e. RR )`
20 4 ffvelrni
` |-  ( x e. ~H -> ( S ` x ) e. ~H )`
21 normcl
` |-  ( ( S ` x ) e. ~H -> ( normh ` ( S ` x ) ) e. RR )`
22 20 21 syl
` |-  ( x e. ~H -> ( normh ` ( S ` x ) ) e. RR )`
23 6 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
24 normcl
` |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )`
25 23 24 syl
` |-  ( x e. ~H -> ( normh ` ( T ` x ) ) e. RR )`
` |-  ( x e. ~H -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) e. RR )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) e. RR )`
28 12 a1i
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normop ` S ) + ( normop ` T ) ) e. RR )`
29 hosval
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
30 4 6 29 mp3an12
` |-  ( x e. ~H -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
31 30 fveq2d
` |-  ( x e. ~H -> ( normh ` ( ( S +op T ) ` x ) ) = ( normh ` ( ( S ` x ) +h ( T ` x ) ) ) )`
32 norm-ii
` |-  ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( normh ` ( ( S ` x ) +h ( T ` x ) ) ) <_ ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) )`
33 20 23 32 syl2anc
` |-  ( x e. ~H -> ( normh ` ( ( S ` x ) +h ( T ` x ) ) ) <_ ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) )`
34 31 33 eqbrtrd
` |-  ( x e. ~H -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) )`
36 nmoplb
` |-  ( ( S : ~H --> ~H /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( S ` x ) ) <_ ( normop ` S ) )`
37 4 36 mp3an1
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( S ` x ) ) <_ ( normop ` S ) )`
38 nmoplb
` |-  ( ( T : ~H --> ~H /\ x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )`
39 6 38 mp3an1
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( T ` x ) ) <_ ( normop ` T ) )`
` |-  ( ( ( ( normh ` ( S ` x ) ) e. RR /\ ( normh ` ( T ` x ) ) e. RR ) /\ ( ( normop ` S ) e. RR /\ ( normop ` T ) e. RR ) ) -> ( ( ( normh ` ( S ` x ) ) <_ ( normop ` S ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
41 9 11 40 mpanr12
` |-  ( ( ( normh ` ( S ` x ) ) e. RR /\ ( normh ` ( T ` x ) ) e. RR ) -> ( ( ( normh ` ( S ` x ) ) <_ ( normop ` S ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
42 22 25 41 syl2anc
` |-  ( x e. ~H -> ( ( ( normh ` ( S ` x ) ) <_ ( normop ` S ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( ( normh ` ( S ` x ) ) <_ ( normop ` S ) /\ ( normh ` ( T ` x ) ) <_ ( normop ` T ) ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) )`
` |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) )`
` |-  ( x e. ~H -> ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )`
` |-  ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) )`