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 | |
|
eigpos.2 | |
||
Assertion | eigposi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eigpos.1 | |
|
2 | eigpos.2 | |
|
3 | oveq2 | |
|
4 | 3 | eleq1d | |
5 | 2 1 | hvmulcli | |
6 | hire | |
|
7 | 1 5 6 | mp2an | |
8 | oveq1 | |
|
9 | 3 8 | eqeq12d | |
10 | 7 9 | bitr4id | |
11 | 4 10 | bitrd | |
12 | 11 | adantr | |
13 | 1 2 | eigrei | |
14 | 12 13 | bitrd | |
15 | 14 | biimpac | |
16 | 15 | adantlr | |
17 | hiidrcl | |
|
18 | 1 17 | mp1i | |
19 | ax-his4 | |
|
20 | 1 19 | mpan | |
21 | 20 | ad2antll | |
22 | 18 21 | elrpd | |
23 | simplr | |
|
24 | 3 | ad2antrl | |
25 | his5 | |
|
26 | 2 1 1 25 | mp3an | |
27 | 16 | cjred | |
28 | 27 | oveq1d | |
29 | 26 28 | eqtrid | |
30 | 24 29 | eqtrd | |
31 | 23 30 | breqtrd | |
32 | 16 22 31 | prodge0ld | |
33 | 16 32 | jca | |