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 HrmOp U HrmOp 0 hop op T 0 hop op U 0 hop op T + op U

Proof

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