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 TA=BAA0AihTA=TAihAB

Proof

Step Hyp Ref Expression
1 eigre.1 A
2 eigre.2 B
3 oveq2 TA=BAAihTA=AihBA
4 his5 BAAAihBA=BAihA
5 2 1 1 4 mp3an AihBA=BAihA
6 3 5 eqtrdi TA=BAAihTA=BAihA
7 oveq1 TA=BATAihA=BAihA
8 ax-his3 BAABAihA=BAihA
9 2 1 1 8 mp3an BAihA=BAihA
10 7 9 eqtrdi TA=BATAihA=BAihA
11 6 10 eqeq12d TA=BAAihTA=TAihABAihA=BAihA
12 1 1 hicli AihA
13 ax-his4 AA00<AihA
14 1 13 mpan A00<AihA
15 14 gt0ne0d A0AihA0
16 2 cjcli B
17 mulcan2 BBAihAAihA0BAihA=BAihAB=B
18 16 2 17 mp3an12 AihAAihA0BAihA=BAihAB=B
19 12 15 18 sylancr A0BAihA=BAihAB=B
20 11 19 sylan9bb TA=BAA0AihTA=TAihAB=B
21 2 cjrebi BB=B
22 20 21 bitr4di TA=BAA0AihTA=TAihAB