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 e. ~H
eigorthi.2 
|- B e. ~H
eigorthi.3 
|- C e. CC
eigorthi.4 
|- D e. CC
Assertion eigorthi 
|- ( ( ( ( T ` A ) = ( C .h A ) /\ ( T ` B ) = ( D .h B ) ) /\ C =/= ( * ` D ) ) -> ( ( A .ih ( T ` B ) ) = ( ( T ` A ) .ih B ) <-> ( A .ih B ) = 0 ) )

Proof

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