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
7 4 6 hoaddcli 
 |-  ( 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
12 9 11 readdcli 
 |-  ( ( 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 )
19 18 adantr 
 |-  ( ( 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 )
26 22 25 readdcld 
 |-  ( x e. ~H -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) e. RR )
27 26 adantr 
 |-  ( ( 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 ) ) ) )
35 34 adantr 
 |-  ( ( 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 ) )
40 le2add 
 |-  ( ( ( ( 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 ) ) ) )
43 42 adantr 
 |-  ( ( 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 ) ) ) )
44 37 39 43 mp2and 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( S ` x ) ) + ( normh ` ( T ` x ) ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) )
45 19 27 28 35 44 letrd 
 |-  ( ( x e. ~H /\ ( normh ` x ) <_ 1 ) -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) )
46 45 ex 
 |-  ( x e. ~H -> ( ( normh ` x ) <_ 1 -> ( normh ` ( ( S +op T ) ` x ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) )
47 15 46 mprgbir 
 |-  ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) )