Metamath Proof Explorer


Theorem eigposi

Description: A sufficient condition (first conjunct pair, that holds when T is a positive operator) for an eigenvalue B (second conjunct pair) to be nonnegative. Remark (ii) in Hughes p. 137. (Contributed by NM, 2-Jul-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigpos.1 A
eigpos.2 B
Assertion eigposi AihTA0AihTATA=BAA0B0B

Proof

Step Hyp Ref Expression
1 eigpos.1 A
2 eigpos.2 B
3 oveq2 TA=BAAihTA=AihBA
4 3 eleq1d TA=BAAihTAAihBA
5 2 1 hvmulcli BA
6 hire ABAAihBAAihBA=BAihA
7 1 5 6 mp2an AihBAAihBA=BAihA
8 oveq1 TA=BATAihA=BAihA
9 3 8 eqeq12d TA=BAAihTA=TAihAAihBA=BAihA
10 7 9 bitr4id TA=BAAihBAAihTA=TAihA
11 4 10 bitrd TA=BAAihTAAihTA=TAihA
12 11 adantr TA=BAA0AihTAAihTA=TAihA
13 1 2 eigrei TA=BAA0AihTA=TAihAB
14 12 13 bitrd TA=BAA0AihTAB
15 14 biimpac AihTATA=BAA0B
16 15 adantlr AihTA0AihTATA=BAA0B
17 hiidrcl AAihA
18 1 17 mp1i AihTA0AihTATA=BAA0AihA
19 ax-his4 AA00<AihA
20 1 19 mpan A00<AihA
21 20 ad2antll AihTA0AihTATA=BAA00<AihA
22 18 21 elrpd AihTA0AihTATA=BAA0AihA+
23 simplr AihTA0AihTATA=BAA00AihTA
24 3 ad2antrl AihTA0AihTATA=BAA0AihTA=AihBA
25 his5 BAAAihBA=BAihA
26 2 1 1 25 mp3an AihBA=BAihA
27 16 cjred AihTA0AihTATA=BAA0B=B
28 27 oveq1d AihTA0AihTATA=BAA0BAihA=BAihA
29 26 28 eqtrid AihTA0AihTATA=BAA0AihBA=BAihA
30 24 29 eqtrd AihTA0AihTATA=BAA0AihTA=BAihA
31 23 30 breqtrd AihTA0AihTATA=BAA00BAihA
32 16 22 31 prodge0ld AihTA0AihTATA=BAA00B
33 16 32 jca AihTA0AihTATA=BAA0B0B