Metamath Proof Explorer


Theorem eigorthi

Description: A necessary and sufficient condition (that holds when T is a Hermitian operator) for two eigenvectors A and B to be orthogonal. Generalization of Equation 1.31 of Hughes p. 49. (Contributed by NM, 23-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses eigorthi.1 A
eigorthi.2 B
eigorthi.3 C
eigorthi.4 D
Assertion eigorthi T A = C A T B = D B C D A ih T B = T A ih B A ih B = 0

Proof

Step Hyp Ref Expression
1 eigorthi.1 A
2 eigorthi.2 B
3 eigorthi.3 C
4 eigorthi.4 D
5 oveq2 T B = D B A ih T B = A ih D B
6 his5 D A B A ih D B = D A ih B
7 4 1 2 6 mp3an A ih D B = D A ih B
8 5 7 eqtrdi T B = D B A ih T B = D A ih B
9 oveq1 T A = C A T A ih B = C A ih B
10 ax-his3 C A B C A ih B = C A ih B
11 3 1 2 10 mp3an C A ih B = C A ih B
12 9 11 eqtrdi T A = C A T A ih B = C A ih B
13 8 12 eqeqan12rd T A = C A T B = D B A ih T B = T A ih B D A ih B = C A ih B
14 1 2 hicli A ih B
15 4 cjcli D
16 mulcan2 D C A ih B A ih B 0 D A ih B = C A ih B D = C
17 15 3 16 mp3an12 A ih B A ih B 0 D A ih B = C A ih B D = C
18 14 17 mpan A ih B 0 D A ih B = C A ih B D = C
19 eqcom D = C C = D
20 18 19 bitrdi A ih B 0 D A ih B = C A ih B C = D
21 20 biimpcd D A ih B = C A ih B A ih B 0 C = D
22 21 necon1d D A ih B = C A ih B C D A ih B = 0
23 22 com12 C D D A ih B = C A ih B A ih B = 0
24 oveq2 A ih B = 0 D A ih B = D 0
25 oveq2 A ih B = 0 C A ih B = C 0
26 3 mul01i C 0 = 0
27 15 mul01i D 0 = 0
28 26 27 eqtr4i C 0 = D 0
29 25 28 eqtrdi A ih B = 0 C A ih B = D 0
30 24 29 eqtr4d A ih B = 0 D A ih B = C A ih B
31 23 30 impbid1 C D D A ih B = C A ih B A ih B = 0
32 13 31 sylan9bb T A = C A T B = D B C D A ih T B = T A ih B A ih B = 0