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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmopf | |
|
2 | eleigveccl | |
|
3 | 1 2 | sylan | |
4 | 3 | adantr | |
5 | eleigveccl | |
|
6 | 1 5 | sylan | |
7 | 6 | adantlr | |
8 | 4 7 | jca | |
9 | eighmre | |
|
10 | 9 | recnd | |
11 | 10 | adantr | |
12 | eighmre | |
|
13 | 12 | recnd | |
14 | 13 | adantlr | |
15 | 11 14 | jca | |
16 | 8 15 | jca | |
17 | 16 | adantrr | |
18 | eigvec1 | |
|
19 | 18 | simpld | |
20 | 1 19 | sylan | |
21 | 20 | adantr | |
22 | eigvec1 | |
|
23 | 22 | simpld | |
24 | 1 23 | sylan | |
25 | 24 | adantlr | |
26 | 21 25 | jca | |
27 | 26 | adantrr | |
28 | 12 | cjred | |
29 | 28 | neeq2d | |
30 | 29 | biimpar | |
31 | 30 | anasss | |
32 | 31 | adantlr | |
33 | 27 32 | jca | |
34 | simpll | |
|
35 | hmop | |
|
36 | 34 4 7 35 | syl3anc | |
37 | 36 | adantrr | |
38 | eigorth | |
|
39 | 38 | biimpa | |
40 | 17 33 37 39 | syl21anc | |