Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for an eigenvalue B to be real. Generalization of Equation 1.30 of Hughes p. 49. (Contributed by NM, 21-Jan-2005) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eigre.1 | |
|
eigre.2 | |
||
Assertion | eigrei | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eigre.1 | |
|
2 | eigre.2 | |
|
3 | oveq2 | |
|
4 | his5 | |
|
5 | 2 1 1 4 | mp3an | |
6 | 3 5 | eqtrdi | |
7 | oveq1 | |
|
8 | ax-his3 | |
|
9 | 2 1 1 8 | mp3an | |
10 | 7 9 | eqtrdi | |
11 | 6 10 | eqeq12d | |
12 | 1 1 | hicli | |
13 | ax-his4 | |
|
14 | 1 13 | mpan | |
15 | 14 | gt0ne0d | |
16 | 2 | cjcli | |
17 | mulcan2 | |
|
18 | 16 2 17 | mp3an12 | |
19 | 12 15 18 | sylancr | |
20 | 11 19 | sylan9bb | |
21 | 2 | cjrebi | |
22 | 20 21 | bitr4di | |