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 
|- ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( A .ih B ) = 0 )

Proof

Step Hyp Ref Expression
1 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
2 eleigveccl 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> A e. ~H )
3 1 2 sylan 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> A e. ~H )
4 3 adantr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> A e. ~H )
5 eleigveccl 
 |-  ( ( T : ~H --> ~H /\ B e. ( eigvec ` T ) ) -> B e. ~H )
6 1 5 sylan 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> B e. ~H )
7 6 adantlr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> B e. ~H )
8 4 7 jca 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( A e. ~H /\ B e. ~H ) )
9 eighmre 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. RR )
10 9 recnd 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )
11 10 adantr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` A ) e. CC )
12 eighmre 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` B ) e. RR )
13 12 recnd 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` B ) e. CC )
14 13 adantlr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( ( eigval ` T ) ` B ) e. CC )
15 11 14 jca 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( ( ( eigval ` T ) ` A ) e. CC /\ ( ( eigval ` T ) ` B ) e. CC ) )
16 8 15 jca 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( ( A e. ~H /\ B e. ~H ) /\ ( ( ( eigval ` T ) ` A ) e. CC /\ ( ( eigval ` T ) ` B ) e. CC ) ) )
17 16 adantrr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( ( A e. ~H /\ B e. ~H ) /\ ( ( ( eigval ` T ) ` A ) e. CC /\ ( ( eigval ` T ) ` B ) e. CC ) ) )
18 eigvec1 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ A =/= 0h ) )
19 18 simpld 
 |-  ( ( T : ~H --> ~H /\ A e. ( eigvec ` T ) ) -> ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) )
20 1 19 sylan 
 |-  ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) -> ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) )
21 20 adantr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) )
22 eigvec1 
 |-  ( ( T : ~H --> ~H /\ B e. ( eigvec ` T ) ) -> ( ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) /\ B =/= 0h ) )
23 22 simpld 
 |-  ( ( T : ~H --> ~H /\ B e. ( eigvec ` T ) ) -> ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) )
24 1 23 sylan 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) )
25 24 adantlr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) )
26 21 25 jca 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) ) )
27 26 adantrr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) ) )
28 12 cjred 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> ( * ` ( ( eigval ` T ) ` B ) ) = ( ( eigval ` T ) ` B ) )
29 28 neeq2d 
 |-  ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) -> ( ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) <-> ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) )
30 29 biimpar 
 |-  ( ( ( T e. HrmOp /\ B e. ( eigvec ` T ) ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) -> ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) )
31 30 anasss 
 |-  ( ( T e. HrmOp /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) )
32 31 adantlr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) )
33 27 32 jca 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) ) /\ ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) ) )
34 simpll 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> T e. HrmOp )
35 hmop 
 |-  ( ( T e. HrmOp /\ A e. ~H /\ B e. ~H ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )
36 34 4 7 35 syl3anc 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ B e. ( eigvec ` T ) ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )
37 36 adantrr 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) )
38 eigorth 
 |-  ( ( ( ( A e. ~H /\ B e. ~H ) /\ ( ( ( eigval ` T ) ` A ) e. CC /\ ( ( eigval ` T ) ` B ) e. CC ) ) /\ ( ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) ) /\ ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )
39 38 biimpa 
 |-  ( ( ( ( ( A e. ~H /\ B e. ~H ) /\ ( ( ( eigval ` T ) ` A ) e. CC /\ ( ( eigval ` T ) ` B ) e. CC ) ) /\ ( ( ( T ` A ) = ( ( ( eigval ` T ) ` A ) .h A ) /\ ( T ` B ) = ( ( ( eigval ` T ) ` B ) .h B ) ) /\ ( ( eigval ` T ) ` A ) =/= ( * ` ( ( eigval ` T ) ` B ) ) ) ) /\ ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) ) -> ( A .ih B ) = 0 )
40 17 33 37 39 syl21anc 
 |-  ( ( ( T e. HrmOp /\ A e. ( eigvec ` T ) ) /\ ( B e. ( eigvec ` T ) /\ ( ( eigval ` T ) ` A ) =/= ( ( eigval ` T ) ` B ) ) ) -> ( A .ih B ) = 0 )