Metamath Proof Explorer


Theorem eigrei

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 A
eigre.2 B
Assertion eigrei T A = B A A 0 A ih T A = T A ih A B

Proof

Step Hyp Ref Expression
1 eigre.1 A
2 eigre.2 B
3 oveq2 T A = B A A ih T A = A ih B A
4 his5 B A A A ih B A = B A ih A
5 2 1 1 4 mp3an A ih B A = B A ih A
6 3 5 eqtrdi T A = B A A ih T A = B A ih A
7 oveq1 T A = B A T A ih A = B A ih A
8 ax-his3 B A A B A ih A = B A ih A
9 2 1 1 8 mp3an B A ih A = B A ih A
10 7 9 eqtrdi T A = B A T A ih A = B A ih A
11 6 10 eqeq12d T A = B A A ih T A = T A ih A B A ih A = B A ih A
12 1 1 hicli A ih A
13 ax-his4 A A 0 0 < A ih A
14 1 13 mpan A 0 0 < A ih A
15 14 gt0ne0d A 0 A ih A 0
16 2 cjcli B
17 mulcan2 B B A ih A A ih A 0 B A ih A = B A ih A B = B
18 16 2 17 mp3an12 A ih A A ih A 0 B A ih A = B A ih A B = B
19 12 15 18 sylancr A 0 B A ih A = B A ih A B = B
20 11 19 sylan9bb T A = B A A 0 A ih T A = T A ih A B = B
21 2 cjrebi B B = B
22 20 21 bitr4di T A = B A A 0 A ih T A = T A ih A B