Metamath Proof Explorer


Theorem eighmorth

Description: Eigenvectors of a Hermitian operator with distinct eigenvalues are orthogonal. Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion eighmorth THrmOpAeigvecTBeigvecTeigvalTAeigvalTBAihB=0

Proof

Step Hyp Ref Expression
1 hmopf THrmOpT:
2 eleigveccl T:AeigvecTA
3 1 2 sylan THrmOpAeigvecTA
4 3 adantr THrmOpAeigvecTBeigvecTA
5 eleigveccl T:BeigvecTB
6 1 5 sylan THrmOpBeigvecTB
7 6 adantlr THrmOpAeigvecTBeigvecTB
8 4 7 jca THrmOpAeigvecTBeigvecTAB
9 eighmre THrmOpAeigvecTeigvalTA
10 9 recnd THrmOpAeigvecTeigvalTA
11 10 adantr THrmOpAeigvecTBeigvecTeigvalTA
12 eighmre THrmOpBeigvecTeigvalTB
13 12 recnd THrmOpBeigvecTeigvalTB
14 13 adantlr THrmOpAeigvecTBeigvecTeigvalTB
15 11 14 jca THrmOpAeigvecTBeigvecTeigvalTAeigvalTB
16 8 15 jca THrmOpAeigvecTBeigvecTABeigvalTAeigvalTB
17 16 adantrr THrmOpAeigvecTBeigvecTeigvalTAeigvalTBABeigvalTAeigvalTB
18 eigvec1 T:AeigvecTTA=eigvalTAAA0
19 18 simpld T:AeigvecTTA=eigvalTAA
20 1 19 sylan THrmOpAeigvecTTA=eigvalTAA
21 20 adantr THrmOpAeigvecTBeigvecTTA=eigvalTAA
22 eigvec1 T:BeigvecTTB=eigvalTBBB0
23 22 simpld T:BeigvecTTB=eigvalTBB
24 1 23 sylan THrmOpBeigvecTTB=eigvalTBB
25 24 adantlr THrmOpAeigvecTBeigvecTTB=eigvalTBB
26 21 25 jca THrmOpAeigvecTBeigvecTTA=eigvalTAATB=eigvalTBB
27 26 adantrr THrmOpAeigvecTBeigvecTeigvalTAeigvalTBTA=eigvalTAATB=eigvalTBB
28 12 cjred THrmOpBeigvecTeigvalTB=eigvalTB
29 28 neeq2d THrmOpBeigvecTeigvalTAeigvalTBeigvalTAeigvalTB
30 29 biimpar THrmOpBeigvecTeigvalTAeigvalTBeigvalTAeigvalTB
31 30 anasss THrmOpBeigvecTeigvalTAeigvalTBeigvalTAeigvalTB
32 31 adantlr THrmOpAeigvecTBeigvecTeigvalTAeigvalTBeigvalTAeigvalTB
33 27 32 jca THrmOpAeigvecTBeigvecTeigvalTAeigvalTBTA=eigvalTAATB=eigvalTBBeigvalTAeigvalTB
34 simpll THrmOpAeigvecTBeigvecTTHrmOp
35 hmop THrmOpABAihTB=TAihB
36 34 4 7 35 syl3anc THrmOpAeigvecTBeigvecTAihTB=TAihB
37 36 adantrr THrmOpAeigvecTBeigvecTeigvalTAeigvalTBAihTB=TAihB
38 eigorth ABeigvalTAeigvalTBTA=eigvalTAATB=eigvalTBBeigvalTAeigvalTBAihTB=TAihBAihB=0
39 38 biimpa ABeigvalTAeigvalTBTA=eigvalTAATB=eigvalTBBeigvalTAeigvalTBAihTB=TAihBAihB=0
40 17 33 37 39 syl21anc THrmOpAeigvecTBeigvecTeigvalTAeigvalTBAihB=0