This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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
12 9 11 hoaddcli 
 |-  ( 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
26 21 23 25 lesubaddi 
 |-  ( ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) ) <-> ( normop ` S ) <_ ( ( normop ` ( S +op T ) ) + ( normop ` T ) ) )
27 19 26 mpbir 
 |-  ( ( normop ` S ) - ( normop ` T ) ) <_ ( normop ` ( S +op T ) )