Metamath Proof Explorer

Theorem leopadd

Description: The sum of two positive operators is positive. Exercise 1(i) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leopadd 
|- ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( 0hop <_op T /\ 0hop <_op U ) ) -> 0hop <_op ( T +op U ) )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. x e. ~H ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) <-> ( A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H 0 <_ ( ( U ` x ) .ih x ) ) )
2 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
3 hmopre 
 |-  ( ( U e. HrmOp /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
4 addge0 
 |-  ( ( ( ( ( T ` x ) .ih x ) e. RR /\ ( ( U ` x ) .ih x ) e. RR ) /\ ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) ) -> 0 <_ ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) )
5 4 ex 
 |-  ( ( ( ( T ` x ) .ih x ) e. RR /\ ( ( U ` x ) .ih x ) e. RR ) -> ( ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) -> 0 <_ ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) ) )
6 2 3 5 syl2an 
 |-  ( ( ( T e. HrmOp /\ x e. ~H ) /\ ( U e. HrmOp /\ x e. ~H ) ) -> ( ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) -> 0 <_ ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) ) )
7 6 anandirs 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) -> 0 <_ ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) ) )
8 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
9 hmopf 
 |-  ( U e. HrmOp -> U : ~H --> ~H )
10 8 9 anim12i 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T : ~H --> ~H /\ U : ~H --> ~H ) )
11 hosval 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( T +op U ) ` x ) = ( ( T ` x ) +h ( U ` x ) ) )
12 11 oveq1d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih x ) = ( ( ( T ` x ) +h ( U ` x ) ) .ih x ) )
13 12 3expa 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih x ) = ( ( ( T ` x ) +h ( U ` x ) ) .ih x ) )
14 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
15 14 adantlr 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( T ` x ) e. ~H )
16 ffvelrn 
 |-  ( ( U : ~H --> ~H /\ x e. ~H ) -> ( U ` x ) e. ~H )
17 16 adantll 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( U ` x ) e. ~H )
18 simpr 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> x e. ~H )
19 ax-his2 
 |-  ( ( ( T ` x ) e. ~H /\ ( U ` x ) e. ~H /\ x e. ~H ) -> ( ( ( T ` x ) +h ( U ` x ) ) .ih x ) = ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) )
20 15 17 18 19 syl3anc 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( T ` x ) +h ( U ` x ) ) .ih x ) = ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) )
21 13 20 eqtrd 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih x ) = ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) )
22 10 21 sylan 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( ( T +op U ) ` x ) .ih x ) = ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) )
23 22 breq2d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( 0 <_ ( ( ( T +op U ) ` x ) .ih x ) <-> 0 <_ ( ( ( T ` x ) .ih x ) + ( ( U ` x ) .ih x ) ) ) )
24 7 23 sylibrd 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) -> 0 <_ ( ( ( T +op U ) ` x ) .ih x ) ) )
25 24 ralimdva 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H ( 0 <_ ( ( T ` x ) .ih x ) /\ 0 <_ ( ( U ` x ) .ih x ) ) -> A. x e. ~H 0 <_ ( ( ( T +op U ) ` x ) .ih x ) ) )
26 1 25 syl5bir 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H 0 <_ ( ( U ` x ) .ih x ) ) -> A. x e. ~H 0 <_ ( ( ( T +op U ) ` x ) .ih x ) ) )
27 leoppos 
 |-  ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )
28 leoppos 
 |-  ( U e. HrmOp -> ( 0hop <_op U <-> A. x e. ~H 0 <_ ( ( U ` x ) .ih x ) ) )
29 27 28 bi2anan9 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( 0hop <_op T /\ 0hop <_op U ) <-> ( A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H 0 <_ ( ( U ` x ) .ih x ) ) ) )
30 hmops 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T +op U ) e. HrmOp )
31 leoppos 
 |-  ( ( T +op U ) e. HrmOp -> ( 0hop <_op ( T +op U ) <-> A. x e. ~H 0 <_ ( ( ( T +op U ) ` x ) .ih x ) ) )
32 30 31 syl 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( 0hop <_op ( T +op U ) <-> A. x e. ~H 0 <_ ( ( ( T +op U ) ` x ) .ih x ) ) )
33 26 29 32 3imtr4d 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( 0hop <_op T /\ 0hop <_op U ) -> 0hop <_op ( T +op U ) ) )
34 33 imp 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ ( 0hop <_op T /\ 0hop <_op U ) ) -> 0hop <_op ( T +op U ) )