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 ) )