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 ) )